(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
id
1
1.
A
: Type
i
:
. Id{
i
} = Id
A
A
By:
NatInd Concl
Generated subgoals:
1
Id{
0} = Id
A
A
1
step
2
2.
i
:
3. 0<
i
4. Id{
i
-1} = Id
A
A
Id{
i
} = Id
A
A
3
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
i:
. Id{
i} = Id 
A
A i:. Id{i} = Id AA Id{0} = Id AA
i-1} = Id AA
Id{i} = Id AA
