Def System == {M:(IdMsgA)| loc:Id. Feasible(M(loc)) }

is mentioned by

Thm* i:Id, M:{M:MsgA| Feasible(M) }. @i: M  System

[m-sys-at_wf]

Try larger context: EventSystems IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html