(6steps total) PrintForm Definitions Lemmas num thy 1 Sections StandardLIB Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: gcd wf 1
1. b : 
  a:. gcd(a;b)  
By: (OnVar `b' (RankInd (i.|i|)  CompNatInd)) THEN (Analyze 0)

Generated subgoal:

1 2. b1:. |b1|<|b|  (a:. gcd(a;b1)  )
3. a : 
  gcd(a;b)  
4 steps

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

(6steps total) PrintForm Definitions Lemmas num thy 1 Sections StandardLIB Doc