next id rupHints restPrf' _ =>
simp only [ite_eq_left_iff, Bool.not_eq_true]
intro rupAddSuccess
rw [← Bool.not_eq_true, imp_false, Classical.not_not] at rupAddSuccess
exact addEmptyCaseSound f f_readyForRupAdd rupHints rupAddSuccess
case intro.h_2
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : DecidableEq α
inst✝¹ : Clause α β
inst✝ : Formula α β σ
action : Action β α
restPrf : List (Action β α)
ih :
  ∀ (f : σ),
    readyForRupAdd f →
      readyForRatAdd f →
        (∀ (a : Action β α), a ∈ restPrf → wellFormedAction a) → lratChecker f restPrf = success → unsatisfiable α f
f : σ
f_readyForRupAdd : readyForRupAdd f
f_readyForRatAdd : readyForRatAdd f
actionWellFormed : wellFormedAction action
restPrfWellFormed : ∀ (a : Action β α), a ∈ restPrf → wellFormedAction a
prf✝ : List (Action β α)
id✝ : Nat
rupHints✝ : Array Nat
tail✝ : List (Action β α)
heq✝ : action :: restPrf = Action.addEmpty id✝ rupHints✝ :: tail✝
⊢ (match performRupAdd f empty rupHints✝ with
      | (fst, checkSuccess) => if checkSuccess = true then success else rup_failure) =
      success →
    unsatisfiable α f
no goals