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