Def @i: x:T initially x = v(j)
Def == if eqof(IdDeq)(j,i) x : T initially x = v else  fi

is mentioned by

Thm* i:Id, T:Type, v:T, x:Id. Thm* @i: x:T Thm* @i: xinitially x = v  Thm* realizes es.(vartype(i;x) r T) Thm* realizes es.& (e:E. loc(e) = i  Id  first(e)  (x when e) = v  T)

[init-rule]

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