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