next heq => simp [negateLiteral, ← heq, h, v_in_c]
case intro.inl.intro.isTrue
n : Nat
p : PosFin n → Bool
c : DefaultClause n
l : Literal (PosFin n)
v : PosFin n
v_in_c : (v, false) ∈ Clause.toList c
pv : p v = false
p'_not_entails_c :
  ((v, false) ∈ Clause.toList c → ¬(if v = l.fst then l.snd else p v) = false) ∧
    ((v, true) ∈ Clause.toList c → ¬(if v = l.fst then l.snd else p v) = true)
h✝ : v = l.fst
h : l.snd = true
⊢ l.negateLiteral ∈ Clause.toList c
no goals