`(P : A * B -> Type) : (forall (a : A) (b : B), P (a, b)) <~> (forall p : A * B, P p) := Build_Equiv _ _ (prod_ind P) _.
Require Import Basics.Overture Basics.Equivalences Basics.PathGroupoids Require Import Types.Empty.