{ 
[T:Type]. [dT:EqDecider(T)]. [L:T List]. [x:T].
L[index(L;x)] = x supposing (x 
L) }
{ Proof }
Definitions occuring in Statement :
l_index: index(L;x),
select: l[i],
uimplies: b supposing a,
uall: [x:A]. B[x],
list: type List,
universe: Type,
equal: s = t,
l_member: (x l),
deq: EqDecider(T)
Definitions :
prop: 
,
and: P 
Q,
lelt: i 
j < k,
member: t T,
int_seg: {i..j
},
exists: 
x:A. B[x],
subtype: S 
T,
all: x:A. B[x],
top: Top,
implies: P 
Q,
iff: P 
Q,
rev_implies: P Q,
uimplies: b supposing a,
uall: [x:A]. B[x],
cand: A c B,
nat: 
,
l_member: (x l),
l_index: index(L;x)
Lemmas :
deq_property,
uiff_inversion,
iff_weakening_uiff,
select_wf,
eqof_wf,
assert_wf,
length_wf1,
le_wf,
top_wf,
length_wf_nat,
non_neg_length,
int_seg_wf,
l_index_wf
\mforall{}[T:Type]. \mforall{}[dT:EqDecider(T)]. \mforall{}[L:T List]. \mforall{}[x:T]. L[index(L;x)] = x supposing (x \mmember{} L)
Date html generated:
2011_08_10-AM-07_51_11
Last ObjectModification:
2011_06_18-AM-08_13_55
Home
Index