all_goals
  constructor
  . simp [Clause.toList, delete_iff, negl_ne_v, v_in_c_del_l]
  . split
    . next heq =>
      simp only [heq, negateLiteral, not, ne_eq, Prod.mk.injEq, true_and] at negl_ne_v
      split at negl_ne_v <;> simp_all
    . next hne =>
      exact pv
case intro.inl.intro.intro.h
n : Nat
p : PosFin n → Bool
c : DefaultClause n
l : Literal (PosFin n)
v : PosFin n
pv : p v = false
negl_ne_v : (v, false) ≠ l.negateLiteral
v_in_c_del_l : (v, false) ∈ c.toList
⊢ (v, false) ∈ Clause.toList (c.delete l.negateLiteral) ∧ (if v = l.fst then l.snd else p v) = false

case intro.inr.intro.intro.h
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
⊢ (v, true) ∈ Clause.toList (c.delete l.negateLiteral) ∧ (if v = l.fst then l.snd else p v) = true
no goals