simp only [not_exists, not_or, not_and] at p'_not_entails_c
n : Nat
p : PosFin n → Bool
c : DefaultClause n
l : Literal (PosFin n)
p_entails_c : ∃ a, (a, false) ∈ Clause.toList c ∧ p a = false ∨ (a, true) ∈ Clause.toList c ∧ p a = true
p'_not_entails_c :
  ¬∃ a,
      (a, false) ∈ Clause.toList c ∧ (if a = l.fst then l.snd else p a) = false ∨
        (a, true) ∈ Clause.toList c ∧ (if a = l.fst then l.snd else p a) = true
⊢ l.negateLiteral ∈ Clause.toList c
n : Nat
p : PosFin n → Bool
c : DefaultClause n
l : Literal (PosFin n)
p_entails_c : ∃ a, (a, false) ∈ Clause.toList c ∧ p a = false ∨ (a, true) ∈ Clause.toList c ∧ p a = true
p'_not_entails_c :
  ∀ (x : PosFin n),
    ((x, false) ∈ Clause.toList c → ¬(if x = l.fst then l.snd else p x) = false) ∧
      ((x, true) ∈ Clause.toList c → ¬(if x = l.fst then l.snd else p x) = true)
⊢ l.negateLiteral ∈ Clause.toList c