Issue154.agda:9,8-16
Multiple definitions of X. Previous definition at
Issue154.agda:8,13-14
when scope checking the declaration
  open A public