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
  [<tg,s,v. f(s(x),v)>]
   (tg@0:Id
   (State(x : A)ma-valtype(k : B  rcv(l; tg) : T; k)
   ((k : B  rcv(l; tg) : T(rcv(l; tg@0))?Void List)) List

By:	AssertBY (x : A  x:Id fp-> Type) Auto THEN AssertBY (k : B  rcv(l; tg) : T  k:Knd fp-> Type) Auto THEN At Type Auto THEN Try (Fold `ma-state` 0) THEN DoSubsume

1	10. x : A  x:Id fp-> Type 11. k : B  rcv(l; tg) : T  k:Knd fp-> Type 12. State(x : A) 13. ma-valtype(k : B  rcv(l; tg) : T; k)   ma-valtype(k : B  rcv(l; tg) : T; k) r B	1 step
2	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	2 steps

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