Definition pathsinv0_to_right' {X} {x y:X} (p:y = x) (r:x = y) : idpath _ = p @ r -> !p = r. Proof. intros e. induction p. exact e. Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.Tactics.