IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
gcd unique a,b,y1,y2:. GCD(a;b;y1) GCD(a;b;y2) (y1 ~ y2)
By:
Unfolds [`gcd_p`;`assoced`] 0 THEN HypBackchain
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html
a,b,y1,y2:
. GCD(a;b;y1) 
GCD(a;b;y2) 
