rw [f'_def]
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : DecidableEq α
inst✝¹ : Clause α β
inst✝ : Formula α β σ
f : σ
f_readyForRupAdd : readyForRupAdd f
f_readyForRatAdd : readyForRatAdd f
c : β
pivot : Literal α
f' : σ
rupHints : Array Nat
ratHints : Array (Nat × Array Nat)
pivot_limplies_c : pivot ∈ Clause.toList c
heq : performRatAdd f c pivot rupHints ratHints = (f', true)
restPrf : List (Action β α)
restPrfWellFormed : ∀ (a : Action β α), a ∈ restPrf → wellFormedAction a
ih :
  ∀ (f : σ),
    readyForRupAdd f →
      readyForRatAdd f →
        (∀ (a : Action β α), a ∈ restPrf → wellFormedAction a) → lratChecker f restPrf = success → unsatisfiable α f
f'_success : lratChecker f' restPrf = success
f'_def : f' = Formula.insert f c
f'_readyForRupAdd : readyForRupAdd f'
⊢ readyForRatAdd f'
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : DecidableEq α
inst✝¹ : Clause α β
inst✝ : Formula α β σ
f : σ
f_readyForRupAdd : readyForRupAdd f
f_readyForRatAdd : readyForRatAdd f
c : β
pivot : Literal α
f' : σ
rupHints : Array Nat
ratHints : Array (Nat × Array Nat)
pivot_limplies_c : pivot ∈ Clause.toList c
heq : performRatAdd f c pivot rupHints ratHints = (f', true)
restPrf : List (Action β α)
restPrfWellFormed : ∀ (a : Action β α), a ∈ restPrf → wellFormedAction a
ih :
  ∀ (f : σ),
    readyForRupAdd f →
      readyForRatAdd f →
        (∀ (a : Action β α), a ∈ restPrf → wellFormedAction a) → lratChecker f restPrf = success → unsatisfiable α f
f'_success : lratChecker f' restPrf = success
f'_def : f' = Formula.insert f c
f'_readyForRupAdd : readyForRupAdd f'
⊢ readyForRatAdd (Formula.insert f c)