induction φ <;> simp [subst, Finset.biUnion_union, *]
ν₁ : Type u_1
ν₂ : Type u_2
ν₃ : Type ?u.5697
f f₁ : ν₁ → PropForm ν₂
f₂ : ν₂ → PropForm ν₃
φ φ₁ φ₂ : PropForm ν₁
inst✝¹ : DecidableEq ν₁
inst✝ : DecidableEq ν₂
⊢ vars (subst φ f) = Finset.biUnion (vars φ) fun v1 => vars (f v1)
no goals