cases hϕ
ν₁ : Type u_1
ν₂ : Type u_2
inst✝² : DecidableEq ν₁
inst✝¹ : DecidableEq ν₂
inst✝ : Fintype ν₁
f : ν₁ → ν₂
φ : PropFun ν₁
hf : Function.Injective f
ϕ : PropForm ν₁
hϕ : ⟦ϕ⟧ = φ
⊢ semVars (map f φ) = Finset.map { toFun := f, inj' := hf } (semVars φ)
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 ⟦ϕ⟧)