IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
hmk pair def1 1. 'a : S
2. 'b : S
3. x : 'a 4. y : 'b mk_pair(x,y) = (a:'a. b:'b. (a =x)(b =y)) ('a'b hbool)
By:
Unab [`hmk_pair`] THEN Simp THEN StrongAuto
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
mk_pair(x,y) = (
a:'a. 
x)
(b =
('a 
'b 
