{z : A} : (forall i, z $-> x i) -> (z $-> cat_prod I x). Proof. apply cate_cat_prod_corec. Defined.
Require Import Basics.Equivalences Basics.Overture Basics.Tactics. Require Import Types.Bool Types.Prod Types.Forall. Require Import WildCat.Bifunctor WildCat.Core WildCat.Equiv WildCat.EquivGpd