module Issue477b where

record D where
  field A : Set