simp [Array.mem_def]
case mk
L : Type u
ν : Type v
inst✝² : LitVar L ν
inst✝¹ inst✝ : DecidableEq ν
x : ν
data : List (Clause L)
h : x ∈ PropFun.semVars (toPropFun { data := data })
⊢ ∃ C ∈ { data := data }, x ∈ PropFun.semVars (Clause.toPropFun C)
case mk
L : Type u
ν : Type v
inst✝² : LitVar L ν
inst✝¹ inst✝ : DecidableEq ν
x : ν
data : List (Clause L)
h : x ∈ PropFun.semVars (toPropFun { data := data })
⊢ ∃ C ∈ data, x ∈ PropFun.semVars (Clause.toPropFun C)