(5steps total)
Remark
PrintForm
Definitions
Lemmas
IteratedBinops
Sections
DiscrMathExt
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
add
via
intseg
addends
3
is_assoc_sep(
; (
x
,
y
.
x
+
y
))
By:
Thm*
is_assoc_sep(
; (
x
,
y
.
x
+
y
)) Asserted
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(5steps total)
Remark
PrintForm
Definitions
Lemmas
IteratedBinops
Sections
DiscrMathExt
Doc