Definition invrot (X:Type) (x y:X) (p:x=y) (p':y=x) : !p = p' -> p = !p'. Proof. intros e. induction e. apply pathsinv0. apply pathsinv0inv0. Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.Tactics.