{z : A} (f : z $-> x) (g : z $-> y) : cat_pr2 $o cat_binprod_corec f g $== g := cat_prod_beta _ _ false.
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