1. a : 
2. p : a
  {x:a| p(x) } ~ (Msize(x.if p(x) 1 else 0 fi))

By:	BackThru:  Thm*  f:(a2).  Thm*  (i:a. P(i)  f(i) = 1  2)  ({x:a| P(x) } ~ (Msize(f))) THEN Reduce Concl

1

i:a. p(i)  if p(i) 1 else 0 fi = 1  2

3 steps

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