---

Step * of Lemma list_decomp

∀[T:Type]. ∀[L:T List].  L ~ [hd(L) / tl(L)] supposing 0 < ||L||
BY
{ (InductionOnList THEN All Reduce THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[L:T  List].    L  \msim{}  [hd(L)  /  tl(L)]  supposing  0  <  ||L||


By

---

Latex:
(InductionOnList  THEN  All  Reduce  THEN  Auto)

---

Home Index