theorem Aesop.BuiltinRules.not_intro {P : Prop} (h : P → False) : ¬P

theorem Aesop.BuiltinRules.empty_false (h : Empty) : False

theorem Aesop.BuiltinRules.pEmpty_false (h : PEmpty) : False

theorem Aesop.BuiltinRules.heq_iff_eq {α : Sort u_1} (x y : α) : x ≍ y ↔ x = y