1. x : 
2. 2x
3. (i:{2..x}. i | x)
4. b : 
5. |b| | x
  (b ~ 1)  (b ~ x)

By:	(Use:[b] Inst: Thm*  a:. |a| ~ a THEN SimilarTo (|b| ~ 1)  (|b| ~ x)) THEN ChainRelation: Thm*  EquivRel x,y:. x ~ y

1

6. |b| ~ b   (|b| ~ 1)  (|b| ~ x)

PREMISE

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