Definition invrot'rot (X:Type) (x y:X) (p:x=y) (p':y=x) (e : !p = p') : invrot' (invrot e) = e. Proof. now induction e,p. Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.Tactics.