proposition: Lemma path_forall_1_beta `{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: Proof. path_forall_beta_t. Defined.
imports: Basics.Overture Basics.Tactics Basics.PathGroupoids Basics.Contractible Basics.Equivalences Types.Prod Types.Forall Tactics.BinderApply