simp only [List.cons.injEq] at hprf
α : 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
c : β
pivot : Literal α
rupHints : Array Nat
ratHints : Array (Nat × Array Nat)
restPrf' : List (Action β α)
hprf : action :: restPrf = Action.addRat id c pivot rupHints ratHints :: restPrf'
x✝ : σ × Bool
f' : σ
checkSuccess : Bool
heq : performRatAdd f c pivot rupHints ratHints = (f', checkSuccess)
hCheckSuccess : checkSuccess = true
f'_success : lratChecker f' restPrf' = success
⊢ unsatisfiable α f
α : 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
c : β
pivot : Literal α
rupHints : Array Nat
ratHints : Array (Nat × Array Nat)
restPrf' : List (Action β α)
x✝ : σ × Bool
f' : σ
checkSuccess : Bool
heq : performRatAdd f c pivot rupHints ratHints = (f', checkSuccess)
hCheckSuccess : checkSuccess = true
f'_success : lratChecker f' restPrf' = success
hprf : action = Action.addRat id c pivot rupHints ratHints ∧ restPrf = restPrf'
⊢ unsatisfiable α f