DiscreteMath
Sections
DiscrMathExt
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Rank
Theorem
Name
9
Thm*
a
,
b
:
. (
A
~
a
)
(
B
~
b
)
((
A
B
) ~
(
a
b
))
[finite_indep_sum_card]
cites the following:
8
Thm*
a
,
b
:
. (
a
b
) ~
(
a
b
)
[nsub_mul_rw]
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
DiscreteMath
Sections
DiscrMathExt
Doc
a,b:
. (A ~ a) 
(B ~ b) ((A
B) ~ (a
b))a,b:. (ab) ~ (ab)a,b:. (A ~ a) (B ~ b) ((AB) ~ (ab))a,b:. (ab) ~ (ab)