We used => before, which is strange, because it has another meaning
in ssreflect.