no goals
F : Type u_3
α : Type u_2
β : Type u_1
γ : Type ?u.30200
δ : Type ?u.30203
inst✝² : HeytingAlgebra α
inst✝¹ : HeytingAlgebra β
inst✝ : HeytingHomClass F α β
f : F
a : α
⊢ ↑f (aᶜ) = ↑f aᶜ
rw [← himp_bot, ← himp_bot, map_himp, map_bot]