clear h
case mk
L : Type u
ν : Type v
inst✝¹ : LitVar L ν
inst✝ : DecidableEq ν
x : ν
data : List L
h : x ∈ PropFun.semVars (toPropFun { data := data })
τ : PropAssignment ν
hpos : τ ⊨ toPropFun { data := data }
hneg : (fun M φ => ¬M ⊨ φ) (PropAssignment.set τ x !τ x) (toPropFun { data := data })
⊢ ∃ l ∈ { data := data }, LitVar.toVar l = x
case mk
L : Type u
ν : Type v
inst✝¹ : LitVar L ν
inst✝ : DecidableEq ν
x : ν
data : List L
τ : PropAssignment ν
hpos : τ ⊨ toPropFun { data := data }
hneg : (fun M φ => ¬M ⊨ φ) (PropAssignment.set τ x !τ x) (toPropFun { data := data })
⊢ ∃ l ∈ { data := data }, LitVar.toVar l = x