a,b,a',b':. b-a = b'-a'  ({a..b} ~ {a'..b'})

1

1. a :  2. b :  3. a' :  4. b' :  5. b-a = b'-a'   f:({a..b}{a'..b'}), g:({a'..b'}{a..b}).   InvFuns({a..b};{a'..b'};f;g)

3 steps

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