let l be Nat; :: thesis: UsedIntLoc (goto l) = {}
( InsCode (goto l) = 6 & not 6 in {1,2,3,4,5} ) by ENUMSET1:def 3, SCMFSA_2:23;
hence UsedIntLoc (goto l) = {} by Def1; :: thesis: verum