oProd :: VProd f n as -> Prod f as
toProd = \case
  Nil     -> Ø
  a :% as -> a :< toProd as


toProd :: VProd f n as -> Prod f as
toProd = \case
  Nil     -> Ø
  a :% as -> a :< toProd as
toProd = \case
  Nil     -> Ø
  a :% as -> a :< toProd as