PrintForm
Definitions
Lemmas
IteratedBinops
Sections
DiscrMathExt
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
zero
ann
iter
via
intseg
a
,
b
:
,
e
:({
a
..
b
}
). (
i
:{
a
..
b
}.
e
(
i
) = 0)
(
i
:{
a
..
b
}.
e
(
i
)) = 0
By:
SimilarTo:
Thm*
(
i
:{
a
..
b
}.
e
(
i
)) = 0
(
i
:{
a
..
b
}.
e
(
i
) = 0) ...
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
PrintForm
Definitions
Lemmas
IteratedBinops
Sections
DiscrMathExt
Doc
a,b:
, e:({a..b
}
i:{a..b
(
i:{a..b
