module Data.Type

data D : Type where