Lemma grinvmaponpathsinv (X : gr) {a b : X} (e : a^-1 = b^-1) : a = b. Proof. assert (e' := maponpaths (λ x, x^-1) e). simpl in e'. rewrite (grinvinv X _) in e'. rewrite (grinvinv X _) in e'. apply e'. Defined.
Require Import UniMath.MoreFoundations.Subtypes.