. split at rupAddSuccess
  . simp only [Prod.mk.injEq, and_false] at rupAddSuccess
  . split at rupAddSuccess
    . simp only [Prod.mk.injEq, and_false] at rupAddSuccess
    . 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
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
rupAddSuccess :
  (if ((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.2.snd = true then
      (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, false)
    else
      if ((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.2.fst = false then
        (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, false)
      else
        ({ 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