have f'_def := rupAdd_result f c rupHints f' f_readyForRupAdd rupAddSuccess
n : Nat
f : DefaultFormula n
c : DefaultClause n
rupHints : Array Nat
f' : DefaultFormula n
f_readyForRupAdd : f.readyForRupAdd
rupAddSuccess : f.performRupAdd c rupHints = (f', true)
⊢ liff (PosFin n) f f'
n : Nat
f : DefaultFormula n
c : DefaultClause n
rupHints : Array Nat
f' : DefaultFormula n
f_readyForRupAdd : f.readyForRupAdd
rupAddSuccess : f.performRupAdd c rupHints = (f', true)
f'_def : f' = f.insert c
⊢ liff (PosFin n) f f'