simp [map, *, PropForm.semVars_map]
case refl
ν₁ : Type u_1
ν₂ : Type u_2
inst✝² : DecidableEq ν₁
inst✝¹ : DecidableEq ν₂
inst✝ : Fintype ν₁
f : ν₁ → ν₂
hf : Function.Injective f
ϕ : PropForm ν₁
⊢ semVars (map f ⟦ϕ⟧) = Finset.map { toFun := f, inj' := hf } (semVars ⟦ϕ⟧)
no goals