a✝ b✝ c d : Prop
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a b : α
h : a = b
⊢ (a == b) = true
a✝ b✝ c d : Prop
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a b : α
⊢ a = b → (a == b) = true
intro h
a✝ b c d : Prop
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
⊢ (a == a) = true
a✝ b✝ c d : Prop
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a b : α
h : a = b
⊢ (a == b) = true
subst h
no goals
a✝ b c d : Prop
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
⊢ (a == a) = true
exact LawfulBEq.rfl