1. A : Type
2. B : Type
3. C : Type
  (ABC) ~ ((AB)C)

By:	Witness: abc.abc/a,bc. bc/b,c. <<a,b>,c> | xyz.xyz/xy,z. xy/x,y. <x,y,z>

1

InvFuns(ABC;(AB)C   InvFuns;abc.abc/a,bc. bc/b,c. <<a,b>,c>;xyz.xyz/xy,z. xy/x,y. <x,y,z>)

9 steps

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