(f : x $-> z) (g : y $-> z) : cat_bincoprod_rec f g $o cat_inr $== g := @cat_binprod_beta_pr2 A^op _ _ _ _ x y _ _ f g.
Require Import Basics.Overture Basics.Tactics Basics.Decidable. Require Import Types.Bool. Require Import WildCat.Core WildCat.Equiv WildCat.Forall WildCat.NatTrans