for l being Nat
for i being Instruction of SCM+FSA holds UsedILoc (l .--> i) = UsedIntLoc i