Agda-2.3.2.2: test/fail/Issue476a.agda

-- Useless private
module Issue476a where

A : Set₁
private
  A = Set