for il being Nat
for dl being Int-Location holds il <> dl