1. Type
2. X : Type
3. eq : EqDecider(X)
4. f : x:X fp-> Type
5. g : x:X fp-> Type
6. x : X
7. f  g
8. x  dom(f)
9. x  dom(g)
10. x1@0 : f(x)
  x1@0  g(x)

1

f(x) = g(x)  Type

1 step

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