Commit 2020-07-09 06:11 c06f500f
View on Github →feat(logic/basic): add eq_iff_true_of_subsingleton (#3308) I'm surprised we didn't have this already.
example (x y : unit) : x = y := by simp
feat(logic/basic): add eq_iff_true_of_subsingleton (#3308) I'm surprised we didn't have this already.
example (x y : unit) : x = y := by simp