(3steps total)
PrintForm
Definitions
Lemmas
IteratedBinops
Sections
DiscrMathExt
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
sum
via
intseg
singleton
1
1
1.
a
:
2.
b
:
3. {
a
..
b
}
4.
a
+1 =
b
is_ident(
; (
x
,
y
.
x
+
y
); 0)
By:
BackThru:
Thm*
is_ident(
; (
x
,
y
.
x
+
y
); 0)
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(3steps total)
PrintForm
Definitions
Lemmas
IteratedBinops
Sections
DiscrMathExt
Doc
}
is_ident(
x,y. x+y); 0)
