for x being Element of NAT
for y being Tuple of LenBSeq x, BOOLEAN st Nat2BL . x = y holds
Absval y = x