PrintForm
Definitions
mb
tree
Sections
MarkB
generic
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
t
iterate
wf
E
,
A
:Type,
l
:(
E
A
),
n
:(
A
A
A
),
t
:Tree(
E
). t_iterate(
l
;
n
;
t
)
A
By:
UnivCD THEN RecUnfold `t_iterate` 0 THEN TreeInd -1
THEN
AllHyps (RecFold `t_iterate`)
THEN
BackThruSomeHyp
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
PrintForm
Definitions
mb
tree
Sections
MarkB
generic
Doc
E,A:Type, l:(E
A), n:(AAA), t:Tree(E). t_iterate(l;n;t) 
A E,A:Type, l:(EA), n:(AAA), t:Tree(E). t_iterate(l;n;t) A
