rename and document fields in shift_rot proof