have f'_def : f' = (performRupCheck f rupHints).1 := rfl
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
rupHints : Array Nat
f' : DefaultFormula n := (f.performRupCheck rupHints).fst
⊢ List.foldl clearUnit (f.performRupCheck rupHints).fst.assignments (f.performRupCheck rupHints).snd.fst = f.assignments
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
⊢ List.foldl clearUnit (f.performRupCheck rupHints).fst.assignments (f.performRupCheck rupHints).snd.fst = f.assignments