P:(0Prop). 
  (i:0. Dec(P(i)))
  
  (n,k:, f:(n0), g:(k0).
  (increasing(f;n)
  (& increasing(g;k)
  (& (i:n. P(f(i)))
  (& (j:k. P(g(j)))
  (& (i:0. (j:n. i = f(j))  (j:k. i = g(j))))

By:	Auto THEN InstConcl [0;0;i.i;i.i] THEN Reduce 0 THEN Easy

None

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