path_forall_2_beta' `{Funext} A B x0 x1 P f g e Px : @transport (forall a : A, B a) (fun f => P (f x0) (f x1)) f g (@path_forall _ _ _ _ _ e) Px = @transport (B x0 * B x1) (fun x => P (fst x) (snd x)) (f x0, f x1) (g x0, g x1) (path_prod' (e x0) (e x1)) Px. Proof. transport_path_forall_hammer. repeat match goal with | [ |- context[e ?x] ] => induction (e x) end; cbn. reflexivity. Qed.
Require Import Basics.Overture Basics.Tactics Basics.PathGroupoids Basics.Contractible Basics.Equivalences. Require Import Types.Prod Types.Forall.