Definition path_inv_rotate_2 {X} {a b c d:X} (p:a = b) (p':c = d) (q:a = c) (q':b = d) : q @ p' = p @ q' -> p' @ ! q' = !q @ p. Proof. induction q,q'. simpl. repeat rewrite pathscomp0rid. apply idfun. Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.Tactics.