simp[LogicalConnective.iff]
F : Type u_1
α : outParam (Type u_2)
β : outParam (Type u_3)
inst✝³ : LogicalConnective α
inst✝² : LogicalConnective β
inst✝¹ : FunLike F α β
inst✝ : HomClass F α β
f : F
a b : α
⊢ f (a ⟷ b) = f a ⟷ f b
no goals