theorem :: SCMFSA9A:8

for I, J being MacroInstruction of SCM+FSA
for a being Int-Location holds UsedI*Loc (if=0 (a,I,J)) = (UsedI*Loc I) \/ (UsedI*Loc J)