fact: Definition ProductResolve (C : Type -> Type) (r : product) : Type := fold_right (fun t acc => match t with | Inj t => C t * acc | Self => acc end)%type unit r.
imports: List String ExtLib.Structures.CoMonad ExtLib.Programming.Show ExtLib.Data.Monads.IdentityMonad ExtLib.Structures.Monads