no goals
F : Type u_3
α : Type u_2
β : Type u_1
γ : Type ?u.33397
δ : Type ?u.33400
inst✝² : HeytingAlgebra α
inst✝¹ : HeytingAlgebra β
inst✝ : HeytingHomClass F α β
f : F
a b : α
⊢ ↑f (a ⇔ b) = ↑f a ⇔ ↑f b
simp_rw [bihimp, map_inf, map_himp]