Nuprl Lemma : make_list_fan_wf
[T:Type]. [A:
T]. [n:]. (make_list_fan(T;A;n) 
T List)
Proof
Definitions occuring in Statement :
make_list_fan: make_list_fan(T;A;n),
nat: ,
uall: [x:A]. B[x],
member: t T,
function: x:A B[x],
universe: Type
Definitions :
make_list_fan: make_list_fan(T;A;n),
member: t T,
nat: ,
uall: [x:A]. B[x],
prop: 
,
and: P 
Q,
lelt: i 
j < k,
int_seg: {i..j
},
guard: {T}
Lemmas :
subtype_rel_self,
nat_wf,
int_seg_wf,
le_wf,
primrec-wf
\mforall{}[T:Type]. \mforall{}[A:\mBbbN{} {}\mrightarrow{} T]. \mforall{}[n:\mBbbN{}]. (make\_list\_fan(T;A;n) \mmember{} T List)
Date html generated:
2013_03_20-AM-09_48_43
Last ObjectModification:
2012_11_27-AM-10_32_02
Home
Index