---

Step * of Lemma ml-length-sq

∀[T:Type]. ∀[l:T List]. (ml-length(l) ~ ||l||) supposing valueall-type(T)
BY
{ (Unfold `ml-length` 0
   THEN InductionOnList
   THEN RW (AddrC [1;1] UnrollRecursionC) 0
   THEN All (RepUR ``spreadcons ml_apply``)
   THEN (Trivial ORELSE ((CallByValueReduce 0 THEN Auto) THEN Reduce 0 THEN RWO "-1" 0 THEN Auto))) }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[l:T  List].  (ml-length(l)  \msim{}  ||l||)  supposing  valueall-type(T)


By

---

Latex:
(Unfold  `ml-length`  0
  THEN  InductionOnList
  THEN  RW  (AddrC  [1;1]  UnrollRecursionC)  0
  THEN  All  (RepUR  ``spreadcons  ml\_apply``)
  THEN  (Trivial  ORELSE  ((CallByValueReduce  0  THEN  Auto)  THEN  Reduce  0  THEN  RWO  "-1"  0  THEN  Auto)))

---

Home Index