{z : A} {f g : forall i, x i $-> z} : (forall i, f i $== g i) -> cat_coprod_rec f $== cat_coprod_rec g := cat_prod_corec_eta I (A:=A^op) (x:=x).
Require Import Basics.Overture Basics.Tactics Basics.Decidable. Require Import Types.Bool. Require Import WildCat.Core WildCat.Equiv WildCat.Forall WildCat.NatTrans