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