a:, P:(aProp), f:(a2).
  (i:a. P(i)  f(i) = 1  2)  ({x:a| P(x) } ~ (Msize(f)))

By:	Def of Msize(<nat>) THEN Reduce Concl THEN Rewrite by Thm*  a:, b:(a). (i:ab(i)) ~ ( i:a. b(i))

1

a:, P:(aProp), f:(a2).   (i:a. P(i)  f(i) = 1  2)  ({x:a| P(x) } ~ (i:a(f(i))))

9 steps

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