(5steps 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 sym 1

1. a : 
2. b : 
  gcd(a;b) ~ gcd(b;a)


By: (Inst Thm* a,b:y:. GCD(a;b;y) & gcd(a;b) = y [a;b])
THEN
(Inst Thm* a,b:y:. GCD(a;b;y) & gcd(a;b) = y [b;a])


Generated subgoal:

1 3. y:. GCD(a;b;y) & gcd(a;b) = y
4. y:. GCD(b;a;y) & gcd(b;a) = y
  gcd(a;b) ~ gcd(b;a)

3 steps

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

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