1. A : Dsys
2. i : Id
3. a : Id
  Dec(a declared in M(i))

1

4. ds : x:Id fp-> Type 5. da : a:Knd fp-> Type 6. x:Id fp-> ds(x)?Void 7. a:Id fp-> State(ds)ma-valtype(da; locl(a))Prop 8. kx:KndId fp-> State(ds)ma-valtype(da; 1of(kx))ds(2of(kx))?Void 9. kl:KndIdLnk fp-> (tg:Id 9. kl:KndIdLnk fp-> (State(ds)ma-valtype(da; 1of(kl)) 9. kl:KndIdLnk fp-> ((da(rcv(2of(kl); tg))?Void List)) List 10. x:Id fp-> Knd List 11. ltg:IdLnkId fp-> Knd List 12. Top   Dec(locl(a)  dom(da))

1 step

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