Definition invrotrot' (X:Type) (x y:X) (p:x=y) (p':y=x) (e : p = !p') : invrot (invrot' e) = e. Proof. rewrite <- (pathsinv0inv0 e). generalize (!e); clear e. intros e. now induction e, p'. Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.Tactics.