for I being really-closed Program of
for k being Nat st k <= card I holds
(Macro (goto k)) ';' I is really-closed