IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
hpair eq 'a,'b:S.
all
(b:'b. all
(b:'b. (a:'a. all
(b:'b. (a:'a. (y:'b. all
(b:'b. (a:'a. (y:'b. (x:'a. equal
(b:'b. (a:'a. (y:'b. (x:'a. (equal(pair(x,y),pair(a,b))
(b:'b. (a:'a. (y:'b. (x:'a. ,and(equal(x,a),equal(y,b)))))))
By:
HOL "hpair_eq"
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html
'a,'b:S.
all
b:'b. all
