fact: Definition stdPathOver' {X:Type} {x x':X} (p:x=x') {Y : X -> Type} (y' : Y x') : PathOver p (transportb Y p y') y'.
imports: UniMath.Foundations.All UniMath.MoreFoundations.Tactics UniMath.MoreFoundations.PartA