1. x : Id
2. k : Knd
3. A : Type
4. T : Type
5. f : ATA
  (s,v. f(s(x),v))  State(x : A)ma-valtype(k : T; k)x : A(x)?Void

1

6. s : State(x : A) 7. v : ma-valtype(k : T; k)   f(s(x),v)  x : A(x)?Void

7 steps

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