Definition path_inverse_from_right' {X} {x y:X} (p q:x = y) : p@!q = idpath _ -> p = q. Proof. intros e. destruct q. intermediate_path (p @ idpath x). { apply pathsinv0. apply pathscomp0rid. } exact e. Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.Notations. Require Import UniMath.MoreFoundations.Tactics.