apply Or.inr
case intro.inr.intro.intro
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, false) ∈ Clause.toList (c.delete l.negateLiteral) ∧ (if v = l.fst then l.snd else p v) = false ∨
    (v, true) ∈ Clause.toList (c.delete l.negateLiteral) ∧ (if v = l.fst then l.snd else p v) = true
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