path_forall_recr_beta' `{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 a, B a) * B x0) (fun x => P (fst x) (snd x)) (f, f x0) (g, g x0) (path_prod' (@path_forall _ _ _ _ _ e) (e x0)) 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.