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