Nuprl - mb_event_system_7 LEMMAs for s_DASH_init_DASH

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html

Rank	Theorem	Name
5	Thm* i:Id, T:Type, v:T, x:Id. Thm* @i: x : T initially x = v Dsys Thm* & (D:Dsys. Thm* & (@i: x : T initially x = v D Thm* & ( Thm* & (D Thm* & (realizes es.(vartype(i;x) r T) Thm* & (realizes es.& (e:E. loc(e) = i Id first(e) (x when e) = v T))	[s-init-rule]
cites the following:
4	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]

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html