(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:
mul
via
intseg
split
mid
2
is_assoc_sep(
; (
x
,
y
.
x
y
))
By:
Analyze THEN Reduce Concl
Generated subgoal:
1
1.
x
:
y@0
,
y
:
.
x
y@0
y
=
x
y@0
y
Auto
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
is_assoc_sep(
; (
x,y. x
y)) is_assoc_sep(; (x,y. xy))
y@0,y:. xy@0y = xy@0y
