proposition: Lemma transportf_bind {X : UU} {P : X → UU} {x x' x'' : X} (e : x' = x) (e' : x = x'') y y' : y = transportf P e y' -> transportf _ e' y = transportf _ (e @ e') y'.
proof: Proof. intro H; destruct e, e'; exact H. Defined.
imports: UniMath.Foundations.All UniMath.MoreFoundations.Tactics