for m being Nat
for x being Tuple of 1, INT st x /. 1 = m holds
x = <*m*>