proposition: Lemma grinvmaponpathsinv (X : gr) {a b : X} (e : paths (grinv X a) (grinv X b)) : a = b.
proof: Proof. assert (e' := maponpaths (λ x, grinv X x) e). simpl in e'. rewrite (grinvinv X _) in e'. rewrite (grinvinv X _) in e'. apply e'. Defined.
imports: UniMath.MoreFoundations.Orders UniMath.MoreFoundations.Tactics UniMath.MoreFoundations.Subtypes UniMath.Algebra.BinaryOperations UniMath.Algebra.Monoids