---

Step * of Lemma length2-decomp

∀[T:Type]. ∀L:T List. ∃a,b:T. ∃L':T List. (L = (L' @ [a; b]) ∈ (T List)) supposing ||L|| ≥ 2 
BY
{ (Auto THEN (InstLemma `append_firstn_lastn_sq` [⌜L⌝;⌜||L|| - 2⌝]⋅ THENA Auto')) }

1
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))

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}L:T  List.  \mexists{}a,b:T.  \mexists{}L':T  List.  (L  =  (L'  @  [a;  b]))  supposing  ||L||  \mgeq{}  2 


By

---

Latex:
(Auto  THEN  (InstLemma  `append\_firstn\_lastn\_sq`  [\mkleeneopen{}L\mkleeneclose{};\mkleeneopen{}||L||  -  2\mkleeneclose{}]\mcdot{}  THENA  Auto'))

---

Home Index