proposition: Lemma 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 (fun y : B x1 => P (g x0) y) (e x1) (transport (fun y : B x0 => P y (f x1)) (e x0) Px).
proof: Proof. transport_path_forall_hammer. reflexivity. Qed.
imports: Basics.Overture Basics.Tactics Basics.PathGroupoids Basics.Contractible Basics.Equivalences Types.Prod Types.Forall Tactics.BinderApply