---

Step * of Lemma nth_tl_decomp_eq

∀[T:Type]. ∀[m:ℕ]. ∀[L:T List].  nth_tl(m;L) = [L[m] / nth_tl(1 + m;L)] ∈ (T List) supposing m < ||L||
BY
{ (((Auto THEN InstLemma `nth_tl_decomp` [T;m;L]) THENM HypSubst (-1) 0) THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[m:\mBbbN{}].  \mforall{}[L:T  List].    nth\_tl(m;L)  =  [L[m]  /  nth\_tl(1  +  m;L)]  supposing  m  <  ||L||


By

---

Latex:
(((Auto  THEN  InstLemma  `nth\_tl\_decomp`  [T;m;L])  THENM  HypSubst  (-1)  0)  THEN  Auto)

---

Home Index