introduced some more local notation in folds_isomorphism to make proofs and statements more readable