PrintForm
Definitions
Lemmas
DiscreteMath
Sections
DiscrMathExt
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
nsub
intseg
rw
a
,
b
:
. {
a
..
b
} ~
(
b
-
a
)
By:
Auto THEN BackThru:
Thm*
c
,
a
:
,
b
:
.
c
=
b
-
a
({
a
..
b
} ~
c
)
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
PrintForm
Definitions
Lemmas
DiscreteMath
Sections
DiscrMathExt
Doc
a,b:
. {a..b
} ~ 
(b-a) a,b:. {a..b} ~ (b-a)c,a:, b:. c = b-a 
({a..b} ~ c)
