have h := insertRupUnits_postcondition f f_readyForRupAdd units
n : Nat
f : DefaultFormula n
f_readyForRupAdd : f.readyForRupAdd
units : List (Literal (PosFin n))
⊢ (f.insertRupUnits units).fst.assignments_invariant
n : Nat
f : DefaultFormula n
f_readyForRupAdd : f.readyForRupAdd
units : List (Literal (PosFin n))
h :
  let assignments := (f.insertRupUnits units).fst.assignments;
  let_fun hsize := ⋯;
  let rupUnits := (f.insertRupUnits units).fst.rupUnits;
  insertUnit_invariant f.assignments ⋯ rupUnits assignments hsize
⊢ (f.insertRupUnits units).fst.assignments_invariant