(2steps total)
PrintForm
Definitions
Lemmas
IteratedBinops
Sections
DiscrMathExt
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Corollary to
mul
via
intseg
factors
At:
exp
reduce1
a
,
b
,
c
:
. (
a
b
)
c
=
a
c
b
c
By:
Auto
Generated subgoal:
1
1.
a
:
2.
b
:
3.
c
:
(
a
b
)
c
=
a
c
b
c
1
step
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(2steps total)
PrintForm
Definitions
Lemmas
IteratedBinops
Sections
DiscrMathExt
Doc
a,b,c:
. (a
b)
c = acbc a,b,c:. (ab)c = acbc
(ab)c = acbc
