theorem Th8: :: SCM_INST:8

SCM-Instr c= [:NAT,(NAT *),(proj2 SCM-Instr):]