. intro incrementalChecker_success p pf
  unfold incrementalLRATChecker at incrementalChecker_success
  simp only at incrementalChecker_success
  split at incrementalChecker_success
  . next rupHints =>
    by_cases performRupAdd_success : (performRupAdd f empty rupHints).2
    . exact addEmptyCaseSound f f_readyForRupAdd rupHints performRupAdd_success p pf
    . simp only [performRupAdd_success, ite_false] at incrementalChecker_success
  . 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
  . next c pivot rupHints ratHints =>
    by_cases performRatAdd_success : (performRatAdd f c pivot rupHints ratHints).2
    . simp only [performRatAdd_success, ite_true] at incrementalChecker_success
    . simp only [performRatAdd_success, ite_false] at incrementalChecker_success
  . simp only at incrementalChecker_success
case left
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : DecidableEq α
inst✝¹ : Clause α β
inst✝ : Formula α β σ
f : σ
f_readyForRupAdd : readyForRupAdd f
f_readyForRatAdd : readyForRatAdd f
a : Action β α
aWellFormed : wellFormedAction a
⊢ (incrementalLRATChecker f a).snd = success → unsatisfiable α f

case right
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : DecidableEq α
inst✝¹ : Clause α β
inst✝ : Formula α β σ
f : σ
f_readyForRupAdd : readyForRupAdd f
f_readyForRatAdd : readyForRatAdd f
a : Action β α
aWellFormed : wellFormedAction a
⊢ (incrementalLRATChecker f a).snd = out_of_proof → unsatisfiable α (incrementalLRATChecker f a).fst → unsatisfiable α f
case right
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : DecidableEq α
inst✝¹ : Clause α β
inst✝ : Formula α β σ
f : σ
f_readyForRupAdd : readyForRupAdd f
f_readyForRatAdd : readyForRatAdd f
a : Action β α
aWellFormed : wellFormedAction a
⊢ (incrementalLRATChecker f a).snd = out_of_proof → unsatisfiable α (incrementalLRATChecker f a).fst → unsatisfiable α f