DiscreteMath
Sections
DiscrMathExt
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Rank
Theorem
Name
6
Thm*
a
,
b
:
. (
a
+
b
) ~
(
a
+
b
)
[nsub_add_rw]
cites the following:
5
Thm*
c
,
a
,
b
:
.
a
+
b
=
c
((
a
+
b
) ~
c
)
[nsub_add]
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
DiscreteMath
Sections
DiscrMathExt
Doc
a,b:
. (a+b) ~ (a+b)c,a,b:. a+b = c 
((a+b) ~ c)a,b:. (a+b) ~ (a+b)c,a,b:. a+b = c ((a+b) ~ c)