induction F <;> simp
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
case mk.cons
L : Type u
ν : Type v
inst✝¹ : LitVar L ν
inst✝ : DecidableEq ν
v : ν
head✝ : Clause L
tail✝ : List (Clause L)
tail_ih✝ :
  v ∈ PropFun.semVars (List.foldr (fun x x_1 => x ⊓ x_1) ⊤ (List.map Clause.toPropFun tail✝)) →
    ∃ C ∈ tail✝, ∃ l ∈ C.data, LitVar.toVar l = v
⊢ v ∈ PropFun.semVars (Clause.toPropFun head✝ ⊓ List.foldr (fun x x_1 => x ⊓ x_1) ⊤ (List.map Clause.toPropFun tail✝)) →
    (∃ l ∈ head✝.data, LitVar.toVar l = v) ∨ ∃ a ∈ tail✝, ∃ l ∈ a.data, LitVar.toVar l = v