fact: Definition prod_coind `(f : forall x:X, A x) `(g : forall x:X, B x) : forall x, A x * B x := prod_coind_uncurried (f, g).
imports: Basics.Overture Basics.Equivalences Basics.PathGroupoids Basics.Tactics Basics.Trunc Basics.Decidable Types.Empty