{A : Type} `{HasEquivs A} {hbc : HasBinaryCoproducts A} {w x y z : A} (f : w $-> z) (g : x $-> z) (h : y $-> z) : cat_bincoprod_rec (cat_bincoprod_rec f g) h $o associator_cat_bincoprod w x y $== cat_bincoprod_rec f (cat_bincoprod_rec g h). Proof. nrapply cate_moveR_eV. symmetry. exact (cat_binprod_associator_corec (HasBinaryProducts0:=hasbinaryproducts_op_hasbinarycoproducts (hbc:=hbc)) f g h). Defined.
Require Import Basics.Overture Basics.Tactics Basics.Decidable. Require Import Types.Bool. Require Import WildCat.Core WildCat.Equiv WildCat.Forall WildCat.NatTrans