module Issue705 where

module A where
  data A : Set where

open A

open A