proposition: Lemma 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 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: Proof. etransitivity. - apply path_forall_recr_beta'. - refine (transport_path_prod' _ _ _ _). Defined.
imports: Basics.Overture Basics.Tactics Basics.PathGroupoids Basics.Contractible Basics.Equivalences Types.Prod Types.Forall Tactics.BinderApply