---

Step * 1 1 of Lemma fseg_select


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
BY
{ ((RWO "select_append_back" 0 THENA Auto) THEN Try ((EqCD THEN Auto)) THEN RWO "length_append" 0 THEN Auto') }

---

Latex:

---

Latex:

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


By

---

Latex:
((RWO  "select\_append\_back"  0  THENA  Auto)
  THEN  Try  ((EqCD  THEN  Auto))
  THEN  RWO  "length\_append"  0
  THEN  Auto')

---

Home Index