P,Q:(Prop), f:({u:| P(u) }{v:| Q(v) }).
  Inj({k:| P(k) }; {k:| Q(k) }; 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 })

1

1. P : Prop 2. Q : Prop 3. f : {u:| P(u) }{v:| Q(v) } 4. Inj({k:| P(k) }; {k:| Q(k) }; f) 5. m : {u:| P(u) } 6. k : {v:| Q(v) }   (Replace value k by f(m) in f)  {u:| P(u) & u = m }{v:| Q(v) & v = k }

7 steps

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