1. P : Prop
2. Q : Prop
3. f : {u:| P(u) }{v:| Q(v) }
4. Inj({u:| P(u) }; {v:| Q(v) }; f)
5. m : {u:| P(u) }
6. k : {v:| Q(v) }
7. (Replace value k by f(m) in f)  {u:| P(u) & u = m }{v:| Q(v) & v = k }
8. a1 : 
9. P(a1) & a1 = m
10. a2 : 
11. P(a2) & a2 = m
12. (Replace value k by f(m) in f)(a1) = (Replace value k by f(m) in f)(a2)
13. f(a1) = k
14. f(a2) = k
  a1 = a2  {u:| P(u) & u = m }

1

15. f(a1) = f(a2)  {v:| Q(v) & v = k }   a1 = a2  {u:| P(u) & u = m }

1 step

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