FTA
Sections
DiscrMathExt
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Rank
Theorem
Name
4
Thm*
a
:
,
b
:
,
f
:({
a
..
b
}
).
{
a
..
b
}(
f
)
[eval_factorization_nat_plus]
cites the following:
3
Thm*
x
,
y
:
.
x
y
[mul_nat_plus]
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
FTA
Sections
DiscrMathExt
Doc
a:
, b:
, f:({a..b
}
). 
{a..b}(f) 
x,y:. x
y a:, b:, f:({a..b}). {a..b}(f) x,y:. xy