fact: Definition unpack_prod `{P : A * B -> Type} (u : A * B) : P (fst u, snd u) -> P u := idmap.
imports: Basics.Overture Basics.Equivalences Basics.PathGroupoids Basics.Tactics Basics.Trunc Basics.Decidable Types.Empty