a,b:. CoPrime(a,b)  (x,y:. ax+by = 1)

By:	RepD THEN (FwdThru Thm* a,b:. CoPrime(a,b)  (x,y:. (ax+by) ~ 1) [-1]) THEN ExRepD

1

1. a :  2. b :  3. CoPrime(a,b) 4. x :  5. y :  6. (ax+by) ~ 1   x,y:. ax+by = 1

4 steps

About: IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html