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 }

By:	Compute Replace value k by f(m) in f THEN Analyze

1

7. i : {u:| P(u) & u = m }   if f(i)=k f(m) else f(i) fi  {v:| Q(v) & v = k }

6 steps

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