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

1

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

2 steps

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