take (intloc 0) := (intloc 0) ; :: thesis: (intloc 0) := (intloc 0) is sequential
thus (intloc 0) := (intloc 0) is sequential ; :: thesis: verum