1. A : Type
2. B : AType
3. C : (x:AB(x))Type
  f:((z:(x:AB(x))C(z))(x:Ay:B(x)C(<x,y>))),
  g:((x:Ay:B(x)C(<x,y>))(z:(x:AB(x))C(z))).
  InvFuns(z:(x:AB(x))C(z);x:Ay:B(x)C(<x,y>);f;g)

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

1

InvFuns(z:(x:AB(x))C(z);x:Ay:B(x)C(<x,y>)   InvFuns;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