(6steps total)
PrintForm
Definitions
Lemmas
DiscreteMath
Sections
DiscrMathExt
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
compose
iter
point
id
A
:Type,
f
:(
A
A
),
u
:
A
.
f
(
u
) =
u
(
i
:
.
f
{
i
}(
u
) =
u
)
By:
Guarding (
i
:<type>. <prop>) (UnivCD ...w
)
Generated subgoal:
1
1.
A
: Type
2.
f
:
A
A
3.
u
:
A
4.
f
(
u
) =
u
i
:
.
f
{
i
}(
u
) =
u
5
steps
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(6steps total)
PrintForm
Definitions
Lemmas
DiscreteMath
Sections
DiscrMathExt
Doc
A:Type, f:(A
A), u:A. f(u) = u 
(i:
. f{
i}(u) = u) A:Type, f:(AA), u:A. f(u) = u (i:. f{i}(u) = u)i:<type>. <prop>) (UnivCD ...w)A
i:. f{i}(u) = u
