next c rupHints =>
by_cases performRupAdd_success : (performRupAdd f c rupHints).2
. simp only [performRupAdd_success, ite_true] at incrementalChecker_success
. simp only [performRupAdd_success, ite_false] at incrementalChecker_success
case left.h_2
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : DecidableEq α
inst✝¹ : Clause α β
inst✝ : Formula α β σ
f : σ
f_readyForRupAdd : readyForRupAdd f
f_readyForRatAdd : readyForRatAdd f
p : α → Bool
pf : p ⊨ f
action✝ : Action β α
id✝ : Nat
c✝ : β
rupHints✝ : Array Nat
aWellFormed : wellFormedAction (Action.addRup id✝ c✝ rupHints✝)
incrementalChecker_success :
  (if (performRupAdd f c✝ rupHints✝).snd = true then ((performRupAdd f c✝ rupHints✝).fst, out_of_proof)
      else ((performRupAdd f c✝ rupHints✝).fst, rup_failure)).snd =
    success
⊢ False
no goals