1. x : 
2. x1:. x1<x  x1!  (given (x1 rem 2) = 0)
  x!  (given (x rem 2) = 0)

By:	Compute x! * if x=0 1 else x(x-2)! fi THEN SplitITE Concl

1	3. x = 0   1  (given (x rem 2) = 0)	Auto
2	3. x  0   x(x-2)!  (given (x rem 2) = 0)	15 steps

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