---

Step * 2 of Lemma bag-member-sv-list


1. T : Type@i'
2. L : T List@i
3. single-valued-list(L;T)
4. x : T@i
5. i : ℕ@i
6. i < ||L|| c∧ (x = L[i] ∈ T)@i
⊢ x ↓∈ L
BY
{ ((D 0 THEN Auto) THEN InstConcl [⌈L⌉]⋅ THEN Auto THEN Unfold `l_member` 0) }

---

Latex:

---

Latex:

1.  T  :  Type@i'
2.  L  :  T  List@i
3.  single-valued-list(L;T)
4.  x  :  T@i
5.  i  :  \mBbbN{}@i
6.  i  <  ||L||  c\mwedge{}  (x  =  L[i])@i
\mvdash{}  x  \mdownarrow{}\mmember{}  L


By

---

Latex:
((D  0  THEN  Auto)  THEN  InstConcl  [\mkleeneopen{}L\mkleeneclose{}]\mcdot{}  THEN  Auto  THEN  Unfold  `l\_member`  0)

---

Home Index