Nuprl - mb_event_system_3 LEMMAs for change_DASH_since_DASH

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

Rank	Theorem	Name
7	Thm* es:ES, x,i:Id, T:Type, c:T. Thm* (x,y:T. Dec(x = y T)) Thm* Thm* (vartype(i;x) r T) Thm* Thm* (e:E. loc(e) = i Id first(e) (x when e) = c T) Thm* Thm* (e':E. Thm* (loc(e') = i Id Thm* ( Thm* ((x after e') = c T Thm* ( Thm* ((ev:E. ev e' & (x after ev) = (x when ev) T))	[change-since-init]
cites the following:
2	Thm* es:ES, e':E. e:E. first(e) & e e'	[es-first-exists]
6	Thm* es:ES, x,i:Id, T:Type. Thm* (x,y:T. Dec(x = y T)) Thm* Thm* (vartype(i;x) r T) Thm* Thm* (e',e:E. Thm* (e e' Thm* ( Thm* (loc(e') = i Id Thm* ( Thm* ((x after e') = (x when e) T Thm* ( Thm* ((ev:E. e ev & ev e' & (x after ev) = (x when ev) T))	[change-lemma]
0	Thm* es:ES, e,e':E. e e' loc(e) = loc(e') Id	[es-le-loc]

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