(4steps total)
PrintForm
Definitions
Lemmas
SimpleMulFacts
Sections
DiscrMathExt
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
only
one
nat
divs
one
1
1
1
1.
b
:
2.
b
| 1
3.
c
:
4. 1 =
b
c
b
= 1
By:
FwdThru:
Thm*
x
,
y
:
.
x
y
= 1
x
= 1 &
y
= 1 on [ 1 =
b
c
] ...
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(4steps total)
PrintForm
Definitions
Lemmas
SimpleMulFacts
Sections
DiscrMathExt
Doc
c
b = 1
c
b = 1
x,y:. xy = 1 
x = 1 & y = 1 on [ 1 = bc ] ...
