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

1

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

5 steps

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