theorem Th8: :: SCM_INST:8
SCM-Instr c= [:NAT,(NAT *),(proj2 SCM-Instr):]