rw [performRupCheck_preserves_assignments_size f rupHints, f_assignments_size]
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
rupHints : Array Nat
f' : DefaultFormula n := (f.performRupCheck rupHints).fst
f'_def : f' = (f.performRupCheck rupHints).fst
⊢ f'.assignments.size = n
no goals