rcases p_entails_c with ⟨v, ⟨v_in_c, pv⟩ | ⟨v_in_c, pv⟩⟩
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
case intro.inl.intro
n : Nat
p : PosFin n → Bool
c : DefaultClause n
l : Literal (PosFin n)
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)
v : PosFin n
v_in_c : (v, false) ∈ Clause.toList c
pv : p v = false
⊢ l.negateLiteral ∈ Clause.toList c

case intro.inr.intro
n : Nat
p : PosFin n → Bool
c : DefaultClause n
l : Literal (PosFin n)
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)
v : PosFin n
v_in_c : (v, true) ∈ Clause.toList c
pv : p v = true
⊢ l.negateLiteral ∈ Clause.toList c