Issue476a.agda:5,1-6,10
Using private here has no effect. Private applies only to
declarations that introduce new identifiers into the module, like
type signatures and data, record, and module declarations.