fact: Definition equiv_uncurry (A B C : Type) : (A -> B -> C) <~> (A * B -> C) := equiv_prod_ind (fun _ => C).
imports: Basics.Overture Basics.Equivalences Basics.PathGroupoids Basics.Tactics Basics.Trunc Basics.Decidable Types.Empty