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