simp [toPropFun, Array.mem_def, PropFun.all]
case mk
L : Type u
ν : Type v
inst✝¹ : LitVar L ν
inst✝ : DecidableEq ν
v : ν
F : List (Clause L)
⊢ v ∈ PropFun.semVars (toPropFun { data := F }) → ∃ C ∈ { data := F }, ∃ l ∈ C, LitVar.toVar l = v
case mk
L : Type u
ν : Type v
inst✝¹ : LitVar L ν
inst✝ : DecidableEq ν
v : ν
F : List (Clause L)
⊢ v ∈ PropFun.semVars (List.foldr (fun x x_1 => x ⊓ x_1) ⊤ (List.map Clause.toPropFun F)) →
    ∃ C ∈ F, ∃ l ∈ C.data, LitVar.toVar l = v