---

Step * 2 of Lemma iseg_append_single


1. [T] : Type
2. l1 : T List
3. l2 : T List
4. x : T
5. l1 = (l2 @ [x]) ∈ (T List)
⊢ ∃l:T List. (0 < ||l|| ∧ (l1 = (l2 @ l) ∈ (T List)) ∧ l ≤ [x])
BY
{ ((InstConcl [⌜[x]⌝])⋅ THEN Auto) }

---

Latex:

---

Latex:

1.  [T]  :  Type
2.  l1  :  T  List
3.  l2  :  T  List
4.  x  :  T
5.  l1  =  (l2  @  [x])
\mvdash{}  \mexists{}l:T  List.  (0  <  ||l||  \mwedge{}  (l1  =  (l2  @  l))  \mwedge{}  l  \mleq{}  [x])


By

---

Latex:
((InstConcl  [\mkleeneopen{}[x]\mkleeneclose{}])\mcdot{}  THEN  Auto)

---

Home Index