module Issue556 (A : Set) (x : A) where

y : A
y = x