ext v2
ν₁ : Type u_1
ν₂ : Type u_2
f✝ : ν₁ → ν₂
φ✝ φ₁ φ₂ : PropForm ν₁
inst✝² : DecidableEq ν₁
inst✝¹ : DecidableEq ν₂
inst✝ : Fintype ν₁
f : ν₁ → ν₂
hf : Function.Injective f
φ : PropForm ν₁
⊢ PropFun.semVars ⟦map f φ⟧ = Finset.map { toFun := f, inj' := hf } (PropFun.semVars ⟦φ⟧)
case a
ν₁ : Type u_1
ν₂ : Type u_2
f✝ : ν₁ → ν₂
φ✝ φ₁ φ₂ : PropForm ν₁
inst✝² : DecidableEq ν₁
inst✝¹ : DecidableEq ν₂
inst✝ : Fintype ν₁
f : ν₁ → ν₂
hf : Function.Injective f
φ : PropForm ν₁
v2 : ν₂
⊢ v2 ∈ PropFun.semVars ⟦map f φ⟧ ↔ v2 ∈ Finset.map { toFun := f, inj' := hf } (PropFun.semVars ⟦φ⟧)