Definition transport_funapp {T} {X Y:T->Type} (f:∏ t, X t -> Y t) (x:∏ t, X t) {t t':T} (p:t = t') : transportf _ p ((f t)(x t)) = (transportf (λ t, X t -> Y t) p (f t)) (transportf _ p (x t)). Proof. intros. induction p. reflexivity. Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.Tactics.