`{Funext} A B x P f g e Px : @transport (forall a : A, B a) (fun f => P (f x)) f g (@path_forall _ _ _ _ _ e) Px = @transport (B x) P (f x) (g x) (e x) Px. Proof. path_forall_beta_t. Defined.
Require Import Basics.Overture Basics.Tactics Basics.PathGroupoids Basics.Contractible Basics.Equivalences. Require Import Types.Prod Types.Forall.