(5steps total)
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
factors
2
is_ident(
; (
x
,
y
.
x
y
); 1)
By:
Thm*
is_ident(
; (
x
,
y
.
x
y
); 1) Asserted
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(5steps total)
PrintForm
Definitions
Lemmas
IteratedBinops
Sections
DiscrMathExt
Doc
is_ident(
; (
x,y. x
y); 1) is_ident(; (x,y. xy); 1); (x,y. xy); 1) Asserted
