simp [h] at h1
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 : ¬(τ ⊨ f x ↔ (PropAssignment.set τ v2 !τ v2) ⊨ f x)
h : τ ⊨ f x
⊢ τ ⊨ f x ∧ (fun M φ => ¬M ⊨ φ) (PropAssignment.set τ v2 !τ v2) (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 : ν₁
h : τ ⊨ f x
h1 : ¬(PropAssignment.set τ v2 !τ v2) ⊨ f x
⊢ τ ⊨ f x ∧ (fun M φ => ¬M ⊨ φ) (PropAssignment.set τ v2 !τ v2) (f x)