IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
card curry simple112 1. A : Type
2. B : Type
3. C : Type
4. e : ABC (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
B
(
x,y. e(x,y)) = e
