---

Step * 2 of Lemma fseg_select


1. [T] : Type
2. l1 : T List
3. l2 : T List
4. (||l1|| ≤ ||l2||) c∧ (∀i:ℕ. l1[i] = l2[(||l2|| - ||l1||) + i] ∈ T supposing i < ||l1||)
⊢ fseg(T;l1;l2)
BY
{ (D (-1) THEN Unfold `fseg` 0) }

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

---

Latex:

---

Latex:

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


By

---

Latex:
(D  (-1)  THEN  Unfold  `fseg`  0)

---

Home Index