PrintForm
Definitions
hol
pair
Sections
HOLlib
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
hpair
wd
'a
,
'b
:S. all(
x
:hprod(
'a
;
'b
). equal(pair(fst(
x
),snd(
x
)),
x
))
By:
HOL "hpair_wd"
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
PrintForm
Definitions
hol
pair
Sections
HOLlib
Doc
'a,'b:S. all(
x:hprod('a; 'b). equal(pair(fst(x),snd(x)),x)) 'a,'b:S. all(x:hprod('a; 'b). equal(pair(fst(x),snd(x)),x))
