(11steps total)
PrintForm
Definitions
DiscreteMath
Sections
DiscrMathExt
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
nsub
inj
lop
typing
a
:
,
b
:
,
f
:(
a
inj
b
).
f
(
a
-1) inj
{
x
:
b
|
x
=
f
(
a
-1) }
By:
Auto
Generated subgoal:
1
1.
a
:
2.
b
:
3.
f
:
a
inj
b
f
(
a
-1) inj
{
x
:
b
|
x
=
f
(
a
-1) }
10
steps
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(11steps total)
PrintForm
Definitions
DiscreteMath
Sections
DiscrMathExt
Doc
a:
, b:, f:(a inj
b). f 
(a-1) inj {x:b| 
x = f(a-1) } a:, b:, f:(a inj b). f (a-1) inj {x:b| x = f(a-1) }
a inj b
f (a-1) inj {x:b| x = f(a-1) }
