simp at ratAddSuccess
case isFalse.isFalse.isFalse.isTrue
n : Nat
f : DefaultFormula n
c : DefaultClause n
pivot : Literal (PosFin n)
rupHints : Array Nat
ratHints : Array (Nat × Array Nat)
f' : DefaultFormula n
f_readyForRatAdd : f.readyForRatAdd
pivot_in_c : pivot ∈ Clause.toList c
f'_def : f' = f.insert c
ratHintsExhaustive_eq_true : f.ratHintsExhaustive pivot ratHints = true
h✝³ : ¬(f.insertRupUnits c.negate).snd = true
h✝² : ¬((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.2.snd = true
h✝¹ : ¬((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.2.fst = true
h✝ :
  (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 =
    false
ratAddSuccess :
  ((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).fst,
      false) =
    (f', true)
⊢ equisat (PosFin n) f f'
no goals