rw [PropFun.mem_semVars] at h
ν₁ : Type u_1
ν₂ : Type u_2
f✝ : ν₁ → ν₂
φ✝ φ₁ φ₂ : PropForm ν₁
inst✝² : DecidableEq ν₁
inst✝¹ : DecidableEq ν₂
inst✝ : Fintype ν₁
f : ν₁ → ν₂
hf : Function.Injective f
φ : PropForm ν₁
v1 : ν₁
left✝ : v1 ∈ vars φ
h : f v1 ∈ PropFun.semVars ⟦map f φ⟧
⊢ ?m.68983
ν₁ : Type u_1
ν₂ : Type u_2
f✝ : ν₁ → ν₂
φ✝ φ₁ φ₂ : PropForm ν₁
inst✝² : DecidableEq ν₁
inst✝¹ : DecidableEq ν₂
inst✝ : Fintype ν₁
f : ν₁ → ν₂
hf : Function.Injective f
φ : PropForm ν₁
v1 : ν₁
left✝ : v1 ∈ vars φ
h✝ : f v1 ∈ PropFun.semVars ⟦map f φ⟧
h : ∃ τ, τ ⊨ ⟦map f φ⟧ ∧ (fun M φ => ¬M ⊨ φ) (PropAssignment.set τ (f v1) !τ (f v1)) ⟦map f φ⟧
⊢ ?m.68983