for l being Nat
for i being Instruction of SCM+FSA holds UsedI*Loc (l .--> i) = UsedInt*Loc i