Theorem: LeanSAT.Model.PropForm.vars_map (LeanSAT/Model/Subst.lean)

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