fact: Definition composePathOverRightInverse {X:Type} {x x':X} {Y : X -> Type} {y : Y x} {y' : Y x'} {p:x=x'} (q : PathOver p y y') : q * q^-1 = cp (!pathsinv0r p) (identityPathOver y).
imports: UniMath.Foundations.All UniMath.MoreFoundations.Tactics UniMath.MoreFoundations.PartA