1. T : Type
2. T' : Type
3. x : Id
4. T
5. a : Id
6. P : TT'Prop
7. T'
8. u:T. Dec(v:T'. P(u,v))
9. a@0 : Id
10. eqof(IdDeq)(a,a@0)  false
11. s : State(<[x],x.T>)
  Dec(v:if eqof(KindDeq)(locl(a),locl(a@0))  false T' else Top fi. 
  P(s(x),v))

1	12. eqof(KindDeq)(locl(a),locl(a@0))  False   s(x)  T	1 step
2	12. eqof(KindDeq)(locl(a),locl(a@0)) 13. True   Dec(v:Top. P(s(x),v))	3 steps

About: IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html