induction φ <;> simp [*, Finset.image_union]
ν₁ : Type u_1
ν₂ : Type u_2
f : ν₁ → ν₂
φ φ₁ φ₂ : PropForm ν₁
inst✝¹ : DecidableEq ν₁
inst✝ : DecidableEq ν₂
⊢ vars (map f φ) = Finset.image f (vars φ)
no goals