intro h
L : Type u
ν : Type v
inst✝² : LitVar L ν
inst✝¹ inst✝ : DecidableEq ν
x : ν
F : Cnf L
⊢ x ∈ PropFun.semVars (toPropFun F) → ∃ C ∈ F, x ∈ PropFun.semVars (Clause.toPropFun C)
L : Type u
ν : Type v
inst✝² : LitVar L ν
inst✝¹ inst✝ : DecidableEq ν
x : ν
F : Cnf L
h : x ∈ PropFun.semVars (toPropFun F)
⊢ ∃ C ∈ F, x ∈ PropFun.semVars (Clause.toPropFun C)