specialize p'_not_entails_c v
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.inl.intro
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)
⊢ l.negateLiteral ∈ Clause.toList c