next hne =>
exact pv
case intro.inr.intro.intro.h.right.isFalse
n : Nat
p : PosFin n → Bool
c : DefaultClause n
l : Literal (PosFin n)
v : PosFin n
pv : p v = true
negl_ne_v : (v, true) ≠ l.negateLiteral
v_in_c_del_l : (v, true) ∈ c.toList
h✝ : ¬v = l.fst
⊢ p v = true
no goals