for I being Program of
for k being Nat holds UsedI*Loc I = UsedI*Loc (Reloc (I,k))