---

Step * of Lemma iseg_extend

∀[T:Type]. ∀l1:T List. ∀v:T. ∀l2:T List.  (l1 ≤ l2 ⇒ l1 @ [v] ≤ l2 supposing ||l1|| < ||l2|| c∧ (l2[||l1||] = v ∈ T))
BY
{ ((((Unfold `iseg` 0 THEN Auto') THEN ExRepD) THEN InstConcl [tl(l)]) THEN Auto) }

1
1. T : Type
2. l1 : T List
3. v : T
4. l2 : T List
5. l : T List
6. l2 = (l1 @ l) ∈ (T List)
7. ||l1|| < ||l2||
8. l2[||l1||] = v ∈ T
⊢ l2 = ((l1 @ [v]) @ tl(l)) ∈ (T List)

---

Latex:

---

Latex:
\mforall{}[T:Type]
    \mforall{}l1:T  List.  \mforall{}v:T.  \mforall{}l2:T  List.
        (l1  \mleq{}  l2  {}\mRightarrow{}  l1  @  [v]  \mleq{}  l2  supposing  ||l1||  <  ||l2||  c\mwedge{}  (l2[||l1||]  =  v))


By

---

Latex:
((((Unfold  `iseg`  0  THEN  Auto')  THEN  ExRepD)  THEN  InstConcl  [tl(l)])  THEN  Auto)

---

Home Index