# Pastebin j3dAUDko
type Vec :: Type -> Nat -> Type
type role Vec representational nominal
data Vec a n where
  VNil  :: Vec a Z
  VCons :: a -> Vec a n -> Vec a (S n)

type SVec0 :: forall a n. Vec a n -> Type
type role SVec0 nominal
data SVec0 a where
  SVNil0 :: SVec0 'VNil
  SVCons0 :: Sing a -> SVec0 b -> SVec0 ('VCons a b)