for I being Element of SCM+FSA-Instr st I `1_3 <= 8 holds
I in SCM-Instr