let {- 1 -} x
    {- 2 -} : {- 3 -} Natural
    = {- 4 -} 1

in  x