have := (PropFun.mem_semVars _ _).mpr ⟨τ,h,hneg l hl⟩
case mk.intro.intro
L : Type u
ν : Type v
inst✝¹ : LitVar L ν
inst✝ : DecidableEq ν
x : ν
data : List L
τ : PropAssignment ν
hneg : ∀ x_1 ∈ data, ¬(PropAssignment.set τ x !τ x) ⊨ LitVar.toPropFun x_1
l : L
hl : l ∈ data
h : τ ⊨ LitVar.toPropFun l
⊢ ∃ l ∈ data, LitVar.toVar l = x
case mk.intro.intro
L : Type u
ν : Type v
inst✝¹ : LitVar L ν
inst✝ : DecidableEq ν
x : ν
data : List L
τ : PropAssignment ν
hneg : ∀ x_1 ∈ data, ¬(PropAssignment.set τ x !τ x) ⊨ LitVar.toPropFun x_1
l : L
hl : l ∈ data
h : τ ⊨ LitVar.toPropFun l
this : x ∈ PropFun.semVars (LitVar.toPropFun l)
⊢ ∃ l ∈ data, LitVar.toVar l = x