---

Step * of Lemma list_2_decomp

∀[T:Type]. ∀[z:T List].  z = [z[0]; z[1]] ∈ (T List) supposing ||z|| = 2 ∈ ℕ
BY
{ (Auto' THEN RepeatFor 3 ((D -2 THEN All Reduce THEN Auto)) THEN Auto') }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[z:T  List].    z  =  [z[0];  z[1]]  supposing  ||z||  =  2


By

---

Latex:
(Auto'  THEN  RepeatFor  3  ((D  -2  THEN  All  Reduce  THEN  Auto))  THEN  Auto')

---

Home Index