---

Step * 1 of Lemma nth_tl_decomp


1. T : Type
2. m : ℤ
⊢ ∀[L:T List]. L ~ [L[0] / tl(L)] supposing 0 < ||L||
BY
{ (((InstLemma `list_decomp` [⌜T⌝]⋅ THENM RepeatFor 2 (ParallelLast)) THENA Auto)
   THEN xxxRWO "select0" 0xxx
   THEN Auto) }

---

Latex:

---

Latex:

1.  T  :  Type
2.  m  :  \mBbbZ{}
\mvdash{}  \mforall{}[L:T  List].  L  \msim{}  [L[0]  /  tl(L)]  supposing  0  <  ||L||


By

---

Latex:
(((InstLemma  `list\_decomp`  [\mkleeneopen{}T\mkleeneclose{}]\mcdot{}  THENM  RepeatFor  2  (ParallelLast))  THENA  Auto)
  THEN  xxxRWO  "select0"  0xxx
  THEN  Auto)

---

Home Index