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