(35steps total) PrintForm Definitions Lemmas mb event system 6 Sections EventSystems Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: init-rule 1 1 2
1. i : Id
2. T : Type
3. v : T
4. x : Id
5. es : ES
6. w : World
7. p : FairFifo
8. PossibleWorld(@i: x:T
8. PossibleWorld(@i: xinitially x = v;w)
9. es = ES(w)
10. vartype(i;x) r T
11. e : E
12. loc(e) = i
13. first(e)
  vartype(loc(e);x) r T
By: HypSubst -2 0 THEN D_ES_Subtype

Generated subgoals:

None

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

(35steps total) PrintForm Definitions Lemmas mb event system 6 Sections EventSystems Doc