proposition: Lemma transportf_transpose_right {X : UU} {P : X → UU} {x x' : X} {e : x = x'} {y : P x} {y' : P x'} : transportb P e y' = y -> y' = transportf P e y.
proof: Proof. induction e; apply idfun. Defined.
imports: UniMath.Foundations.All UniMath.MoreFoundations.Tactics