Lemma fginv_fginv {X : hSet} (l : free_monoid (setcoprod X X)) : fginv (fginv l) = l. Proof. unfold fginv. rewrite map_reverse, reverse_reverse, <- map_compose, <- map_idfun. apply map_homot. exact coprodcomm_coprodcomm. Defined.
Require Import UniMath.MoreFoundations.Subtypes. Require Import UniMath.MoreFoundations.Sets. Require Import UniMath.Algebra.Monoids. Require Import UniMath.Algebra.Groups. Require Import UniMath.Algebra.IteratedBinaryOperations. Require Import UniMath.Combinatorics.Lists.