for a, b, c being Int-Location
for f being FinSeq-Location holds not (f,c) := b destroys a