no goals
ι : Type ?u.44592
α : Type u_1
β : Type ?u.44598
π : ι → Type ?u.44603
inst✝ : GeneralizedHeytingAlgebra α
a✝ b✝ c d a b : α
h : Codisjoint a b
⊢ a ⇔ b = a ⊓ b
rw [bihimp, h.himp_eq_left, h.himp_eq_right]