1. A : Type
2. B : AType
3. P : x:AB(x)Prop
4. x:A. y:B(x). y is the y:B(x). P(x,y)
5. f:(x:AB(x)). x:A. f(x) is the y:B(x). P(x,y)
  f:(x:AB(x)). x:A. P(x,f(x))

1

5. f : x:AB(x) 6. x : A 7. f(x) is the y:B(x). P(x,y)   P(x,f(x))

1 step

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