1. A : Type
2. B : AType
3. C : (x:AB(x))Type
  (xy:(x:AB(x))C(xy)) ~ (x:Ay:B(x)C(<x,y>))

By:	(xyz.xyz/xy,z. xy/x,y. <x,y,z>)  (xy:(x:AB(x))C(xy))(x:Ay:B(x)C(<x,y>)) | (xyz.xyz/x,yz. yz/y,z. <<x,y>,z>)  (x:Ay:B(x)C(<x,y>))(xy:(x:AB(x))C(xy)) Asserted THEN Witness: xyz.xyz/xy,z. xy/x,y. <x,y,z> | xyz.xyz/x,yz. yz/y,z. <<x,y>,z>

1	(xyz.xyz/xy,z. xy/x,y. <x,y,z>)    (xy:(x:AB(x))C(xy))(x:Ay:B(x)C(<x,y>))	2 steps
2	4. (xyz.xyz/xy,z. xy/x,y. <x,y,z>) 4.  (xy:(x:AB(x))C(xy))(x:Ay:B(x)C(<x,y>)) 5. (xyz.xyz/x,yz. yz/y,z. <<x,y>,z>) 5.  (x:Ay:B(x)C(<x,y>))(xy:(x:AB(x))C(xy))   InvFuns(xy:(x:AB(x))C(xy);x:Ay:B(x)C(<x,y>)   InvFuns;xyz.xyz/xy,z. xy/x,y. <x,y,z>;xyz.xyz/x,yz. yz/y,z. <<x,y>,z>)	1 step

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