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
  f(m) = f(m)  {v:| Q(v) & v = k }

1

9. f(m)  {v:| Q(v) }   f(m)  {v:| Q(v) & v = k }

3 steps

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