---

Step * 1 1 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)
5. ||nth_tl(||L|| - 2;L)|| = 2 ∈ ℤ
⊢ ∃a,b:T. (nth_tl(||L|| - 2;L) = [a; b] ∈ (T List))
BY
{ (MoveToConcl (-1) THEN (GenConclAtAddr [1;2;1] THENA Auto)) }

1
1. [T] : Type
2. L : T List
3. ||L|| ≥ 2 
4. L ~ firstn(||L|| - 2;L) @ nth_tl(||L|| - 2;L)
5. v : T List
6. nth_tl(||L|| - 2;L) = v ∈ (T List)
⊢ (||v|| = 2 ∈ ℤ) ⇒ (∃a,b:T. (v = [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)
5.  ||nth\_tl(||L||  -  2;L)||  =  2
\mvdash{}  \mexists{}a,b:T.  (nth\_tl(||L||  -  2;L)  =  [a;  b])


By

---

Latex:
(MoveToConcl  (-1)  THEN  (GenConclAtAddr  [1;2;1]  THENA  Auto))

---

Home Index