Library UniMath.Folds.aux_lemmas