`{Funext} A B x0 P f g e Px : @transport (forall a : A, B a) (fun f => P f (f x0)) f g (@path_forall _ _ _ _ _ e) Px = @transport (forall x : A, B x) (fun x => P x (g x0)) f g (@path_forall H A B f g e) (@transport (B x0) (fun y => P f y) (f x0) (g x0) (e x0) Px). Proof. etransitivity. - apply '. - refine (transport_path_prod' _ _ _ _). Defined.
Require Import Basics.Overture Basics.Tactics Basics.PathGroupoids Basics.Contractible Basics.Equivalences. Require Import Types.Prod Types.Forall.