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. intro H; destruct e, e'; exact H. Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.Tactics.