simp at hsat hunsat
case refl.refl.intro.intro
ν₁ : Type u_1
ν₂ : Type u_2
φ φ₁ φ₂ : PropFun ν₁
f✝ f₁ : ν₁ → PropFun ν₂
τ✝ : PropAssignment ν₂
v : ν₁
inst✝¹ : DecidableEq ν₁
inst✝ : DecidableEq ν₂
f : ν₁ → PropFun ν₂
v2 : ν₂
p : PropForm ν₁
f'' : ν₁ → PropForm ν₂
hf' : Quotient.choice f = ⟦f''⟧
τ : PropAssignment ν₂
hsat : τ ⊨ PropForm.subst p f''
hunsat : ¬(PropAssignment.set τ v2 !τ v2) ⊨ PropForm.subst p f''
⊢ ∃ a ∈ semVars ⟦p⟧, v2 ∈ semVars (f a)
case refl.refl.intro.intro
ν₁ : Type u_1
ν₂ : Type u_2
φ φ₁ φ₂ : PropFun ν₁
f✝ f₁ : ν₁ → PropFun ν₂
τ✝ : PropAssignment ν₂
v : ν₁
inst✝¹ : DecidableEq ν₁
inst✝ : DecidableEq ν₂
f : ν₁ → PropFun ν₂
v2 : ν₂
p : PropForm ν₁
f'' : ν₁ → PropForm ν₂
hf' : Quotient.choice f = ⟦f''⟧
τ : PropAssignment ν₂
hsat : PropAssignment.subst (fun x => ⟦f'' x⟧) τ ⊨ p
hunsat : ¬PropAssignment.subst (fun x => ⟦f'' x⟧) (PropAssignment.set τ v2 !τ v2) ⊨ p
⊢ ∃ a ∈ semVars ⟦p⟧, v2 ∈ semVars (f a)