next performRupCheck_success =>
rw [Bool.not_eq_false] at performRupCheck_success
have f_limplies_fc := performRupCheck_of_insertRup_entails_safe_insert f f_readyForRupAdd c rupHints performRupCheck_success
rw [liff_iff_limplies_and_limplies f f', f'_def]
constructor
. exact f_limplies_fc
. exact limplies_of_insert f c
case isFalse.isFalse.isFalse
n : Nat
f : DefaultFormula n
c : DefaultClause n
rupHints : Array Nat
f' : DefaultFormula n
f_readyForRupAdd : f.readyForRupAdd
f'_def : f' = f.insert c
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 = false
rupAddSuccess :
  ({ clauses := ((f.insertRupUnits c.negate).fst.performRupCheck rupHints).1.clauses,
              rupUnits := ((f.insertRupUnits c.negate).fst.performRupCheck rupHints).1.rupUnits,
              ratUnits := ((f.insertRupUnits c.negate).fst.performRupCheck rupHints).1.ratUnits,
              assignments :=
                restoreAssignments ((f.insertRupUnits c.negate).fst.performRupCheck rupHints).1.assignments
                  ((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.fst }.clearRupUnits.insert
        c,
      true) =
    (f', true)
⊢ liff (PosFin n) f f'
no goals