Theorem lawful_beq_subsingleton

Modification history

2024-04-19 20:51

Mathlib/Logic/Basic.lean

chore(Logic): reduce use of autoImplicit (#12135) …

Modified lawful_beq_subsingleton View on Github →

2024-03-21 23:59

Mathlib/Logic/Basic.lean

feat: let `congr!` discharge equalities of `BEq` instances (#11179) …

Added lawful_beq_subsingleton View on Github →