. intro incrementalChecker_res incrementalChecker_res_unsat
  unfold incrementalLRATChecker at incrementalChecker_res
  simp only at incrementalChecker_res
  split at incrementalChecker_res
  . next rupHints =>
    by_cases h : (performRupAdd f empty rupHints).2
    . simp only [h, ite_true] at incrementalChecker_res
    . simp only [Bool.not_eq_true] at h
      simp only [h, ite_false] at incrementalChecker_res
  . next c rupHints =>
    by_cases performRupAdd_success : (performRupAdd f c rupHints).2
    . let f' := (performRupAdd f c rupHints).1
      have heq : performRupAdd f c rupHints = (f', true) := by rw [← performRupAdd_success]
      have f_liff_f' := rupAdd_sound f c rupHints f' f_readyForRupAdd heq
      unfold incrementalLRATChecker at incrementalChecker_res_unsat
      simp only [performRupAdd_success, ite_true] at incrementalChecker_res_unsat
      rw [liff_unsat f f' f_liff_f']
      exact incrementalChecker_res_unsat
    . simp only [Bool.not_eq_true] at performRupAdd_success
      simp only [performRupAdd_success, ite_false] at incrementalChecker_res
  . next c pivot rupHints ratHints =>
    by_cases performRatAdd_success : (performRatAdd f c pivot rupHints ratHints).2
    . let f' := (performRatAdd f c pivot rupHints ratHints).1
      have heq : performRatAdd f c pivot rupHints ratHints = (f', true) := by rw [← performRatAdd_success]
      simp only [wellFormedAction, limplies_iff_mem] at aWellFormed
      unfold incrementalLRATChecker at incrementalChecker_res_unsat
      simp only [performRatAdd_success, ite_true] at incrementalChecker_res_unsat
      have h := ratAdd_sound f c pivot rupHints ratHints f' f_readyForRatAdd aWellFormed heq
      rw [equisat] at h
      rw [h]
      exact incrementalChecker_res_unsat
    . simp only [Bool.not_eq_true] at performRatAdd_success
      simp only [performRatAdd_success, ite_false] at incrementalChecker_res
  . next ids =>
    unfold incrementalLRATChecker at incrementalChecker_res_unsat
    simp only at incrementalChecker_res_unsat
    intro p pf
    exact incrementalChecker_res_unsat p (limplies_delete p pf)
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
no goals