mathlib3
1533f158 - feat(logic/basic): add eq_true_eq_id (#11341)

Commit
4 years ago
feat(logic/basic): add eq_true_eq_id (#11341) Adds the simp lemma `eq_true_eq_id : eq true = id`, a sort of curried version of `eq_true : (a = true) = a` in core.
Author
Parents
Loading