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'. Proof. induction e; apply idfun. Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.Tactics.