rcases p_entails_cl with ⟨v, ⟨⟨negl_ne_v, v_in_c_del_l⟩, pv⟩ | ⟨⟨negl_ne_v, v_in_c_del_l⟩, pv⟩⟩
  <;> [
      (apply Exists.intro v; apply Or.inl);
      (apply Exists.intro v; apply Or.inr)
    ]
n : Nat
p : PosFin n → Bool
c : DefaultClause n
l : Literal (PosFin n)
p_entails_cl :
  ∃ a,
    ((a, false) ≠ l.negateLiteral ∧ (a, false) ∈ c.toList) ∧ p a = false ∨
      ((a, true) ≠ l.negateLiteral ∧ (a, true) ∈ c.toList) ∧ p a = true
⊢ ∃ a,
    (a, false) ∈ Clause.toList (c.delete l.negateLiteral) ∧ (if a = l.fst then l.snd else p a) = false ∨
      (a, true) ∈ Clause.toList (c.delete l.negateLiteral) ∧ (if a = l.fst then l.snd else p a) = true
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