have f'_def := ratAdd_result f c pivot rupHints ratHints f' f_readyForRatAdd pivot_in_c ratAddSuccess
n : Nat
f : DefaultFormula n
c : DefaultClause n
pivot : Literal (PosFin n)
rupHints : Array Nat
ratHints : Array (Nat × Array Nat)
f' : DefaultFormula n
f_readyForRatAdd : f.readyForRatAdd
pivot_in_c : pivot ∈ Clause.toList c
ratAddSuccess : f.performRatAdd c pivot rupHints ratHints = (f', true)
⊢ equisat (PosFin n) f f'
n : Nat
f : DefaultFormula n
c : DefaultClause n
pivot : Literal (PosFin n)
rupHints : Array Nat
ratHints : Array (Nat × Array Nat)
f' : DefaultFormula n
f_readyForRatAdd : f.readyForRatAdd
pivot_in_c : pivot ∈ Clause.toList c
ratAddSuccess : f.performRatAdd c pivot rupHints ratHints = (f', true)
f'_def : f' = f.insert c
⊢ equisat (PosFin n) f f'