simp only [performRupCheck, Prod.mk.eta]
n : Nat
f : DefaultFormula n
f_assignments_invariant : f.assignments_invariant
rupHints : Array Nat
⊢ (f.performRupCheck rupHints).fst.assignments_invariant
n : Nat
f : DefaultFormula n
f_assignments_invariant : f.assignments_invariant
rupHints : Array Nat
⊢ { clauses := f.clauses, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
      assignments :=
        (Array.foldl (confirmRupHint f.clauses) (f.assignments, [], false, false) rupHints
            0).fst }.assignments_invariant