---

Step * 1 1 1 of Lemma iseg_append_single


1. T : Type
2. l1 : T List
3. l2 : T List
4. x : T
5. u : T
6. v : T List
7. 0 < ||v|| + 1
8. l1 = (l2 @ [u / v]) ∈ (T List)
9. [u / v] ≤ [x]
⊢ [u / v] = [x] ∈ (T List)
BY
{ ((((RWO "cons_iseg" (-1)) THEN Auto THEN EqCD THEN Auto THEN (RWO "iseg_nil" (-1))) THENA Auto)
   THEN DVar `v'
   THEN All Reduce
   THEN Auto) }

---

Latex:

---

Latex:

1.  T  :  Type
2.  l1  :  T  List
3.  l2  :  T  List
4.  x  :  T
5.  u  :  T
6.  v  :  T  List
7.  0  <  ||v||  +  1
8.  l1  =  (l2  @  [u  /  v])
9.  [u  /  v]  \mleq{}  [x]
\mvdash{}  [u  /  v]  =  [x]


By

---

Latex:
((((RWO  "cons\_iseg"  (-1))  THEN  Auto  THEN  EqCD  THEN  Auto  THEN  (RWO  "iseg\_nil"  (-1)))  THENA  Auto)
  THEN  DVar  `v'
  THEN  All  Reduce
  THEN  Auto)

---

Home Index