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