simp only [heq, negateLiteral, not, ne_eq, Prod.mk.injEq, true_and] at negl_ne_v
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
heq : v = l.fst
⊢ l.snd = true
n : Nat
p : PosFin n → Bool
c : DefaultClause n
l : Literal (PosFin n)
v : PosFin n
pv : p v = true
v_in_c_del_l : (v, true) ∈ c.toList
heq : v = l.fst
negl_ne_v :
  ¬true =
      match l.snd with
      | true => false
      | false => true
⊢ l.snd = true