---

Step * 1 of Lemma length2-decomp


1. [T] : Type
2. L : T List
3. ||L|| ≥ 2 
4. L ~ firstn(||L|| - 2;L) @ nth_tl(||L|| - 2;L)
⊢ ∃a,b:T. ∃L':T List. (L = (L' @ [a; b]) ∈ (T List))
BY
{ Assert ⌜∃a,b:T. (nth_tl(||L|| - 2;L) = [a; b] ∈ (T List))⌝⋅ }

1
.....assertion..... 
1. [T] : Type
2. L : T List
3. ||L|| ≥ 2 
4. L ~ firstn(||L|| - 2;L) @ nth_tl(||L|| - 2;L)
⊢ ∃a,b:T. (nth_tl(||L|| - 2;L) = [a; b] ∈ (T List))

2
1. [T] : Type
2. L : T List
3. ||L|| ≥ 2 
4. L ~ firstn(||L|| - 2;L) @ nth_tl(||L|| - 2;L)
5. ∃a,b:T. (nth_tl(||L|| - 2;L) = [a; b] ∈ (T List))
⊢ ∃a,b:T. ∃L':T List. (L = (L' @ [a; b]) ∈ (T List))

---

Latex:

---

Latex:

1.  [T]  :  Type
2.  L  :  T  List
3.  ||L||  \mgeq{}  2 
4.  L  \msim{}  firstn(||L||  -  2;L)  @  nth\_tl(||L||  -  2;L)
\mvdash{}  \mexists{}a,b:T.  \mexists{}L':T  List.  (L  =  (L'  @  [a;  b]))


By

---

Latex:
Assert  \mkleeneopen{}\mexists{}a,b:T.  (nth\_tl(||L||  -  2;L)  =  [a;  b])\mkleeneclose{}\mcdot{}

---

Home Index