(43steps total) PrintForm Definitions Lemmas mb event system 7 Sections EventSystems Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: s-pre-init-rule1 1

1. Id
2. Id
3. x : Id
4. A : Type
5. T : Type
6. A
7. P : ATProp
  (s,vP(s(x),v))  State(x : A)TProp


By: Analyze


Generated subgoals:

1 8. s : State(x : A)
  (v.P(s(x),v))  TProp

5 steps
2   State(x : A Type
1 step

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

(43steps total) PrintForm Definitions Lemmas mb event system 7 Sections EventSystems Doc