ι : Type ?u.73381
α : Type u_1
β : Type ?u.73387
inst✝ : GeneralizedHeytingAlgebra α
a b c d : α
h : Codisjoint a b
⊢ b ⇨ a = ⊤ ⇨ a
ι : Type ?u.73381
α : Type u_1
β : Type ?u.73387
inst✝ : GeneralizedHeytingAlgebra α
a b c d : α
h : Codisjoint a b
⊢ b ⇨ a = a
conv_rhs => rw [← @top_himp _ _ a]
no goals
ι : Type ?u.73381
α : Type u_1
β : Type ?u.73387
inst✝ : GeneralizedHeytingAlgebra α
a b c d : α
h : Codisjoint a b
⊢ b ⇨ a = ⊤ ⇨ a
rw [← h.eq_top, sup_himp_self_left]