Def @i: only L affects x : t(j)
Def == if eqof(IdDeq)(j,i) only members of L affect x :t else  fi

is mentioned by

Thm* i:Id, L:Knd List, x:Id, T:Type. Thm* @i: only L affects x : T  Thm* realizes es.(vartype(i;x) r T) Thm* realizes es.& (e:E.  Thm* realizes es.& (loc(e) = i  Id Thm* realizes es.& ( Thm* realizes es.& (((x after e) = (x when e)  T  (kind(e)  L)) Thm* realizes es.& (& ((kind(e)  L)  (x after e) = (x when e)  T))

[frame-rule]

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