simp_all [toPropFun, Array.mem_def]
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
case mk
L : Type u
ν : Type v
inst✝¹ : LitVar L ν
inst✝ : DecidableEq ν
x : ν
data : List L
τ : PropAssignment ν
hpos : ∃ a ∈ data, τ ⊨ LitVar.toPropFun a
hneg : ∀ x_1 ∈ data, ¬(PropAssignment.set τ x !τ x) ⊨ LitVar.toPropFun x_1
⊢ ∃ l ∈ data, LitVar.toVar l = x