rcases this with (h|h)
L : Type u
ν : Type v
inst✝¹ : LitVar L ν
inst✝ : DecidableEq ν
v : ν
hd : Clause L
tl : List (Clause L)
ih :
  v ∈ PropFun.semVars (List.foldr (fun x x_1 => x ⊓ x_1) ⊤ (List.map Clause.toPropFun tl)) →
    ∃ C ∈ tl, ∃ l ∈ C.data, LitVar.toVar l = v
hv : v ∈ PropFun.semVars (Clause.toPropFun hd ⊓ List.foldr (fun x x_1 => x ⊓ x_1) ⊤ (List.map Clause.toPropFun tl))
this :
  v ∈ PropFun.semVars (Clause.toPropFun hd) ∨
    v ∈ PropFun.semVars (List.foldr (fun x x_1 => x ⊓ x_1) ⊤ (List.map Clause.toPropFun tl))
⊢ (∃ l ∈ hd.data, LitVar.toVar l = v) ∨ ∃ a ∈ tl, ∃ l ∈ a.data, LitVar.toVar l = v
case inl
L : Type u
ν : Type v
inst✝¹ : LitVar L ν
inst✝ : DecidableEq ν
v : ν
hd : Clause L
tl : List (Clause L)
ih :
  v ∈ PropFun.semVars (List.foldr (fun x x_1 => x ⊓ x_1) ⊤ (List.map Clause.toPropFun tl)) →
    ∃ C ∈ tl, ∃ l ∈ C.data, LitVar.toVar l = v
hv : v ∈ PropFun.semVars (Clause.toPropFun hd ⊓ List.foldr (fun x x_1 => x ⊓ x_1) ⊤ (List.map Clause.toPropFun tl))
h : v ∈ PropFun.semVars (Clause.toPropFun hd)
⊢ (∃ l ∈ hd.data, LitVar.toVar l = v) ∨ ∃ a ∈ tl, ∃ l ∈ a.data, LitVar.toVar l = v

case inr
L : Type u
ν : Type v
inst✝¹ : LitVar L ν
inst✝ : DecidableEq ν
v : ν
hd : Clause L
tl : List (Clause L)
ih :
  v ∈ PropFun.semVars (List.foldr (fun x x_1 => x ⊓ x_1) ⊤ (List.map Clause.toPropFun tl)) →
    ∃ C ∈ tl, ∃ l ∈ C.data, LitVar.toVar l = v
hv : v ∈ PropFun.semVars (Clause.toPropFun hd ⊓ List.foldr (fun x x_1 => x ⊓ x_1) ⊤ (List.map Clause.toPropFun tl))
h : v ∈ PropFun.semVars (List.foldr (fun x x_1 => x ⊓ x_1) ⊤ (List.map Clause.toPropFun tl))
⊢ (∃ l ∈ hd.data, LitVar.toVar l = v) ∨ ∃ a ∈ tl, ∃ l ∈ a.data, LitVar.toVar l = v