by_cases h : (performRupAdd f empty rupHints).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
action✝ : Action β α
id✝ : Nat
rupHints : Array Nat
aWellFormed : wellFormedAction (Action.addEmpty id✝ rupHints)
incrementalChecker_res_unsat : unsatisfiable α (incrementalLRATChecker f (Action.addEmpty id✝ rupHints)).fst
incrementalChecker_res :
  (if (performRupAdd f empty rupHints).snd = true then ((performRupAdd f empty rupHints).fst, success)
      else ((performRupAdd f empty rupHints).fst, rup_failure)).snd =
    out_of_proof
⊢ unsatisfiable α f
case pos
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : DecidableEq α
inst✝¹ : Clause α β
inst✝ : Formula α β σ
f : σ
f_readyForRupAdd : readyForRupAdd f
f_readyForRatAdd : readyForRatAdd f
action✝ : Action β α
id✝ : Nat
rupHints : Array Nat
aWellFormed : wellFormedAction (Action.addEmpty id✝ rupHints)
incrementalChecker_res_unsat : unsatisfiable α (incrementalLRATChecker f (Action.addEmpty id✝ rupHints)).fst
incrementalChecker_res :
  (if (performRupAdd f empty rupHints).snd = true then ((performRupAdd f empty rupHints).fst, success)
      else ((performRupAdd f empty rupHints).fst, rup_failure)).snd =
    out_of_proof
h : (performRupAdd f empty rupHints).snd = true
⊢ unsatisfiable α f

case neg
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : DecidableEq α
inst✝¹ : Clause α β
inst✝ : Formula α β σ
f : σ
f_readyForRupAdd : readyForRupAdd f
f_readyForRatAdd : readyForRatAdd f
action✝ : Action β α
id✝ : Nat
rupHints : Array Nat
aWellFormed : wellFormedAction (Action.addEmpty id✝ rupHints)
incrementalChecker_res_unsat : unsatisfiable α (incrementalLRATChecker f (Action.addEmpty id✝ rupHints)).fst
incrementalChecker_res :
  (if (performRupAdd f empty rupHints).snd = true then ((performRupAdd f empty rupHints).fst, success)
      else ((performRupAdd f empty rupHints).fst, rup_failure)).snd =
    out_of_proof
h : ¬(performRupAdd f empty rupHints).snd = true
⊢ unsatisfiable α f