1. a : Id
2. T : Type
3. ds : x:Id fp-> Type
4. State(ds)TProp
5. x : {a@0:Id| (a@0  [a]) }
6. State(ds)
  if eqof(KindDeq)(locl(a),locl(x))  false T else Top fi  T

1

7. eqof(KindDeq)(locl(a),locl(x)) 8. true   Top  T

3 steps

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