IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
card curry112 1. A : Type
2. B : AType
3. C : (x:AB(x))Type
4. e : x:Ay:B(x)C(<x,y>)
(x,y. e(x,y)) = e
By:
2 Times (FunExtensionality THEN Reduce Concl)
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Type
B(x))
(
x,y. e(x,y)) = e
