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

By:	SimilarTo: Thm*  f:(A inj B), a:A. f  {x:A| x = a }{y:B| y = f(a) } THEN Analyze-3

1

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) }

7 steps

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