A,A':Type, B:(AType), B':(A'Type).
  (x:A. B(x)) ~ (x':A'. B'(x'))  (x':A'. B'(x')) ~ (x:A. B(x))

1

1. A : Type 2. A' : Type 3. B : AType 4. B' : A'Type 5. (x:A. B(x)) ~ (x':A'. B'(x'))   (x':A'. B'(x')) ~ (x:A. B(x))

14 steps

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