proposition: Lemma free_monoid_extend_homot {X : hSet} {Y : monoid} {f f' : X → Y} (h : f ~ f') : free_monoid_extend f ~ free_monoid_extend f'.
proof: Proof. intro x. apply (maponpaths iterop_list_mon). exact (map_homot h x). Defined.
imports: UniMath.MoreFoundations.Subtypes UniMath.MoreFoundations.Sets UniMath.Algebra.Monoids UniMath.Algebra.Groups UniMath.Algebra.IteratedBinaryOperations UniMath.Combinatorics.Lists