no goals
ι : Type ?u.74711
α : Type u_1
β : Type ?u.74717
inst✝ : GeneralizedHeytingAlgebra α
a b c d : α
h : Codisjoint a b
⊢ b ⇨ a ⊓ b = a
rw [himp_inf_distrib, himp_self, inf_top_eq, h.himp_eq_right]