induction' n with n ih <;> simp[*, conj]
β : Type u_3
α : Type u_1
inst✝³ : LogicalConnective α
inst✝² : LogicalConnective β
F : Type u_2
n : ℕ
inst✝¹ : FunLike F α β
inst✝ : LogicalConnective.HomClass F α β
f : F
v : Fin n → α
⊢ f (conj v) = conj (⇑f ∘ v)
no goals