no goals
ι : Type ?u.38627
α : Type u_1
β : Type ?u.38633
π : ι → Type ?u.38638
inst✝ : GeneralizedHeytingAlgebra α
a✝ b✝ c d a b : α
h : b ≤ a
⊢ a ⇔ b = a ⇨ b
rw [bihimp, himp_eq_top_iff.2 h, top_inf_eq]