1. x : Id
2. tg : Id
3. k : Knd
4. l : IdLnk
5. T : Type
6. A : Type
7. B : Type
8. f : AB(T List)
9. rcv(l; tg) = k  T = B
10. x : A  x:Id fp-> Type
11. k : B  rcv(l; tg) : T  k:Knd fp-> Type
12. s : State(x : A)
13. v : ma-valtype(k : B  rcv(l; tg) : T; k)
14. f(s(x),v) = f(s(x),v)
15. T List
16. T List
17. T
  T r k : B  rcv(l; tg) : T(rcv(l; tg))?Void

By:	RWO Thm* eq:EqDecider(A), f,g:a:A fp-> Top, x:A, z:Top. Thm* f  g(x)?z ~ if x  dom(f) f(x)?z else g(x)?z fi 0 THEN SplitOnConclITE THEN Reduce 0 THEN RWO Thm* eq:EqDecider(A), x,y:A, v:Top. x  dom(y : v)  x = y -1 THEN AssertBY (k : B  k:Knd fp-> Type) Auto THEN HypSubst -2 0 THEN Reduce 0

1

18. rcv(l; tg) = k 19. k : B  k:Knd fp-> Type   T r B

1 step

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