{I A : Type} (x : I -> A) `{Is1Cat A} {H' : Product I x} : Coproduct I (A:=A^op) x := H'.
Require Import Basics.Overture Basics.Tactics Basics.Decidable. Require Import Types.Bool. Require Import WildCat.Core WildCat.Equiv WildCat.Forall WildCat.NatTrans