1. A : Type
2. B : Type
3. T : Type
4. x : Id
5. a : Knd
6. tg : Id
7. l : IdLnk
8. f : AB(T List)
9. a = rcv(l; tg)  T = B
10. x : A  x:Id fp-> Type
11. a : B  x:Knd fp-> Type
12. s : State(x : A)
13. v : if a  dom(a : B) B else rcv(l; tg) : T(a)?Top fi
14. f(s(x),v) = f(s(x),v)
15. T List
16. T List
17. u : T
18. rcv(l; tg)  dom(a : B)
  u  a : B(rcv(l; tg))?Void

By:	RWO Thm* eq:EqDecider(A), x,y:A, v:Top. x  dom(y : v)  x = y -1 THEN DoSubsume THEN SubtypeRelEq THEN HypSubst -1 0 THEN Reduce 0 THEN BackThruSomeHyp

None

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