'a,'b:S, P:('b), rep:('a'b), abs:('b'a).
  iso_pair('a;'b;P;rep;abs)
  
  (a:'a. abs(rep(a)) = a) & (r:'b. P(r) = ((rep(abs(r))) = r))

1

'a,'b:S, P:('b), rep:('a'b), abs:('b'a).   iso_pair('a;'b;P;rep;abs)      (a:'a. abs(rep(a)) = a) & (r:'b. P(r) = ((rep(abs(r))) = r))

13 steps

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