rw [mem_semVars]
case h
ν₁ : Type u_1
ν₂ : Type u_2
φ φ₁ φ₂ : PropFun ν₁
f✝ f₁ : ν₁ → PropFun ν₂
τ✝ : PropAssignment ν₂
v : ν₁
inst✝¹ : DecidableEq ν₁
inst✝ : DecidableEq ν₂
f : ν₁ → PropFun ν₂
v2 : ν₂
p : PropForm ν₁
τ : PropAssignment ν₂
x : ν₁
h1 : PropAssignment.subst (fun x => f x) τ x ≠ PropAssignment.subst (fun x => f x) (PropAssignment.set τ v2 !τ v2) x
⊢ v2 ∈ semVars (f x)
case h
ν₁ : Type u_1
ν₂ : Type u_2
φ φ₁ φ₂ : PropFun ν₁
f✝ f₁ : ν₁ → PropFun ν₂
τ✝ : PropAssignment ν₂
v : ν₁
inst✝¹ : DecidableEq ν₁
inst✝ : DecidableEq ν₂
f : ν₁ → PropFun ν₂
v2 : ν₂
p : PropForm ν₁
τ : PropAssignment ν₂
x : ν₁
h1 : PropAssignment.subst (fun x => f x) τ x ≠ PropAssignment.subst (fun x => f x) (PropAssignment.set τ v2 !τ v2) x
⊢ ∃ τ, τ ⊨ f x ∧ (fun M φ => ¬M ⊨ φ) (PropAssignment.set τ v2 !τ v2) (f x)