X:. 
  prime(X)
  
  (X1:. X1<X  prime(X1)  (a,b:. X1 | ab  X1 | a  X1 | b))
  
  (W:. 0<W  W<X  (t:. X | tW  X | t))

By:	Auto THEN RemoveGuards Concl ...w

1

1. X :  2. prime(X) 3. X1:. X1<X  prime(X1)  (a,b:. X1 | ab  X1 | a  X1 | b)   W:. 0<W  W<X  (t:. X | tW  X | t)

19 steps

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