{ 
[B1,a1:Type]. [r:
(a1 
B1)]. [n:]. (run-to-n(r;n) 
a1 List) }
{ Proof }
Definitions occuring in Statement :
run-to-n: run-to-n(r;n),
uall: [x:A]. B[x],
member: t T,
function: x:A B[x],
product: x:A B[x],
list: type List,
int: ,
universe: Type
Definitions :
uall: [x:A]. B[x],
member: t T,
run-to-n: run-to-n(r;n),
top: Top,
all: x:A. B[x],
subtype: S 
T,
int_seg: {i..j
}
Lemmas :
map_wf,
int_seg_wf,
upto_wf,
pi1_wf_top
\mforall{}[B1,a1:Type]. \mforall{}[r:\mBbbZ{} {}\mrightarrow{} (a1 \mtimes{} B1)]. \mforall{}[n:\mBbbZ{}]. (run-to-n(r;n) \mmember{} a1 List)
Date html generated:
2011_08_17-PM-07_05_18
Last ObjectModification:
2011_06_18-PM-12_47_41
Home
Index