no goals
F : Type u_3
α : Type u_2
β : Type u_1
γ : Type ?u.37721
δ : Type ?u.37724
inst✝² : CoheytingAlgebra α
inst✝¹ : CoheytingAlgebra β
inst✝ : CoheytingHomClass F α β
f : F
a : α
⊢ ↑f (￢a) = ￢↑f a
rw [← top_sdiff', ← top_sdiff', map_sdiff, map_top]