Definition transportf_transpose_left {X : UU} {P : X → UU} {x x' : X} {e : x = x'} {y : P x} {y' : P x'} : y = transportb P e y' → transportf P e y = y'. Proof. induction e; apply idfun. Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.Tactics.