[7,<*l,a*>] in SCM-Instr R by Th7;
hence [7,<*l,a*>] is Instruction of by Def1; :: thesis: verum