1. A : Type
2. B : Type
3. f : AB
4. Inj(A; B; f)
5. a : A
6. f  {x:A| x = a }{y:B| y = f(a) }
  f  {x:A| x = a } inj {y:B| y = f(a) }

By:	ApFun: f  AB to: a

1

7. f(a)  B   f  {x:A| x = a } inj {y:B| y = f(a) }

6 steps

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