fact: Definition transportb_transpose_right {A : UU} {P : A → UU} {x x' : A} {e : x = x'} {y : P x} {y' : P x'} : transportf P e y = y' → y = transportb P e y'.
imports: UniMath.Foundations.All UniMath.MoreFoundations.Tactics