theorem :: SCMFSA8C:50
for a, b, c being Int-Location st a <> b holds
not AddTo (c,b) refers a