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

1

6. x:A. P(x,f(x)) 7. g:(x:AB(x)). (x:A. P(x,g(x)))  g = f   !{f:(x:AB(x))| x:A. P(x,f(x)) }

2 steps

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