P,Q:(Prop), f:({u:| P(u) }{v:| Q(v) }).
  Inj({u:| P(u) }; {v:| Q(v) }; f)
  
  (m:{u:| P(u) }, k:{v:| Q(v) }.
  ((Replace value k by f(m) in f)
  ( {u:| P(u) & u = m }{v:| Q(v) & v = k }
  (& Inj({u:| P(u) & u = m }; {v:| Q(v) & v = k };
  (& Inj(Replace value k by f(m) in f))

1

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 }   Inj({u:| P(u) & u = m }; {v:| Q(v) & v = k };   Inj(Replace value k by f(m) in f)

10 steps

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