rcases h with ⟨c', c'_in_f, pc'⟩
case mp
n : Nat
f : DefaultFormula n
f_readyForRatAdd : f.readyForRatAdd
c : DefaultClause n
pivot : Literal (PosFin n)
rupHints : Array Nat
ratHints : Array (Nat × Array Nat)
pivot_in_c : pivot ∈ Clause.toList c
ratHintsExhaustive_eq_true : f.ratHintsExhaustive pivot ratHints = true
performRatCheck_fold_success :
  (Array.foldl
        (fun x ratHint => if x.snd = true then x.fst.performRatCheck pivot.negateLiteral ratHint else (x.fst, false))
        (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).snd =
    true
p : PosFin n → Bool
h : ∃ x, x ∈ f.toList ∧ ¬((Clause.toList x).any fun l => decide (p l.fst = l.snd)) = true
pfc :
  ∀ (x : DefaultClause n), x ∈ (f.insert c).toList → ((Clause.toList x).any fun l => decide (p l.fst = l.snd)) = true
⊢ False
case mp.intro.intro
n : Nat
f : DefaultFormula n
f_readyForRatAdd : f.readyForRatAdd
c : DefaultClause n
pivot : Literal (PosFin n)
rupHints : Array Nat
ratHints : Array (Nat × Array Nat)
pivot_in_c : pivot ∈ Clause.toList c
ratHintsExhaustive_eq_true : f.ratHintsExhaustive pivot ratHints = true
performRatCheck_fold_success :
  (Array.foldl
        (fun x ratHint => if x.snd = true then x.fst.performRatCheck pivot.negateLiteral ratHint else (x.fst, false))
        (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).snd =
    true
p : PosFin n → Bool
pfc :
  ∀ (x : DefaultClause n), x ∈ (f.insert c).toList → ((Clause.toList x).any fun l => decide (p l.fst = l.snd)) = true
c' : DefaultClause n
c'_in_f : c' ∈ f.toList
pc' : ¬((Clause.toList c').any fun l => decide (p l.fst = l.snd)) = true
⊢ False