num
thy
1
Sections
StandardLIB
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Rank
Theorem
Name
4
Thm*
a
,
b
:
.
a
|
b
&
b
|
a
a
=
b
[assoc_reln]
cites the following:
3
Thm*
a
,
b
:
.
a
|
b
b
|
a
a
=
b
[divides_anti_sym]
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
num
thy
1
Sections
StandardLIB
Doc
a,b:
. a | b & b | a 
a = 
ba,b:. a | b 
b | a a = ba,b:. a | b & b | a a = ba,b:. a | b b | a a = b