rw [← rupAddSuccess] at f'_def
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : DecidableEq α
inst✝¹ : Clause α β
inst✝ : Formula α β σ
f : σ
f_readyForRupAdd : readyForRupAdd f
rupHints : Array Nat
rupAddSuccess : (performRupAdd f empty rupHints).snd = true
f' : σ := (performRupAdd f empty rupHints).fst
f'_def : performRupAdd f empty rupHints = (f', true) → f' = Formula.insert f empty
⊢ unsatisfiable α f
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : DecidableEq α
inst✝¹ : Clause α β
inst✝ : Formula α β σ
f : σ
f_readyForRupAdd : readyForRupAdd f
rupHints : Array Nat
rupAddSuccess : (performRupAdd f empty rupHints).snd = true
f' : σ := (performRupAdd f empty rupHints).fst
f'_def : performRupAdd f empty rupHints = (f', (performRupAdd f empty rupHints).snd) → f' = Formula.insert f empty
⊢ unsatisfiable α f