(5steps total) PrintForm Definitions DiscreteMath Sections DiscrMathExt Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: card curry
  A:Type, B:(AType), C:((x:AB(x))Type).
  (z:(x:AB(x))C(z)) ~ (x:Ay:B(x)C(<x,y>))
By: Def of <type> ~ <type>

Generated subgoal:

1 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)
4 steps

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

(5steps total) PrintForm Definitions DiscreteMath Sections DiscrMathExt Doc