HepLean Documentation

Aesop.BuiltinRules

theorem Aesop.BuiltinRules.not_intro {P : Prop} (h : PFalse) :
theorem Aesop.BuiltinRules.heq_iff_eq {α : Sort u_1} (x y : α) :
HEq x y x = y