complete the rearrangement case of restructuring lens proof
check for backwards definitions compared to the proofs
put restructuring lens example before the definition
improve notation a bit: use indices that don't look like variables for the families of bijections in the restructuring lens