---

Step * 1 of Lemma fseg_select


1. T : Type
2. l1 : T List
3. l2 : T List
4. fseg(T;l1;l2)
5. i : ℕ
6. i < ||l1||
⊢ l1[i] = l2[(||l2|| - ||l1||) + i] ∈ T
BY
{ (D (-3) THEN StrongHypSubst (-3) 0) }

1
1. T : Type
2. l1 : T List
3. l2 : T List
4. L : T List
5. l2 = (L @ l1) ∈ (T List)
6. i : ℕ
7. i < ||l1||
⊢ l1[i] = L @ l1[(||L @ l1|| - ||l1||) + i] ∈ T

---

Latex:

---

Latex:

1.  T  :  Type
2.  l1  :  T  List
3.  l2  :  T  List
4.  fseg(T;l1;l2)
5.  i  :  \mBbbN{}
6.  i  <  ||l1||
\mvdash{}  l1[i]  =  l2[(||l2||  -  ||l1||)  +  i]


By

---

Latex:
(D  (-3)  THEN  StrongHypSubst  (-3)  0)

---

Home Index