1. A : Type
2. B : Type
3. C : Type
  f:((ABC)ABC), g:((ABC)ABC). InvFuns(ABC;ABC;f;g)

By:	Witness: e,x,y. e(<x,y>) | e,z. z/x,y. e(x,y)

1

InvFuns(ABC;ABC;e,x,y. e(<x,y>);e,z. z/x,y. e(x,y))

3 steps

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