IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
coprime intro a,b:. (c:. c | ac | bc | 1) CoPrime(a,b)
By:
(RepUnfolds [`coprime`;`gcd_p`] 0)
THEN
(Backchain [`new_hyps`;Thm*a:. 1 | a])
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:
. (
c | b 
