---

{ [T:Type]. [dT:EqDecider(T)]. [L:T List]. [x:T].
    index(L;x)  ||L|| supposing (x  L) }

{ Proof }

---

Definitions occuring in Statement :  l_index: index(L;x),  length: ||as||,  int_seg: {i..j},  uimplies: b supposing a,  uall: [x:A]. B[x],  member: t  T,  list: type List,  natural_number: $n,  universe: Type,  l_member: (x  l),  deq: EqDecider(T)
Definitions :  member: t  T,  l_index: index(L;x),  top: Top,  all: x:A. B[x],  subtype: S  T,  exists: x:A. B[x],  int_seg: {i..j},  lelt: i  j < k,  and: P  Q,  prop: ,  uall: [x:A]. B[x],  uimplies: b supposing a,  l_member: (x  l),  nat: ,  cand: A c B,  rev_implies: P  Q,  iff: P  Q,  implies: P  Q
Lemmas :  mu-bound,  length_wf_nat,  top_wf,  eqof_wf,  select_wf,  int_seg_wf,  length_wf1,  l_member_wf,  deq_wf,  le_wf,  assert_wf,  iff_weakening_uiff,  uiff_inversion,  deq_property

---

\mforall{}[T:Type].  \mforall{}[dT:EqDecider(T)].  \mforall{}[L:T  List].  \mforall{}[x:T].    index(L;x)  \mmember{}  \mBbbN{}||L||  supposing  (x  \mmember{}  L)


Date html generated: 2011_08_10-AM-07_51_03
Last ObjectModification: 2011_06_18-AM-08_13_51

Home Index