---

Step * of Lemma ml-select-sq

∀[T:Type]. ∀[L:T List]. ∀[n:ℤ].  (ml-select(n;L) ~ L[n]) supposing valueall-type(T)
BY
{ (InductionOnList
   THEN (UnivCD THENA Auto)
   THEN Unfold `ml-select` 0
   THEN (RW (AddrC [1] (LemmaC `ml_apply-sq`))0 THEN Auto)
   THEN RW (AddrC [1;1] (LemmaC `ml_apply-sq`))0
   THEN Auto
   THEN RW (SweepUpC UnrollRecursionC) 0
   THEN Reduce 0
   THEN Fold `ml-select` 0
   THEN Try ((RecUnfold `select` 0 THEN (RWO "-2" 0 THENA Auto)))) }

1
1. T : Type
2. valueall-type(T)
3. n : ℤ
⊢ let x,y = [] 
  in if n <z 1 then x else ml-select(n - 1;y) fi  ~ ⊥

2
1. T : Type
2. valueall-type(T)
3. u : T
4. v : T List
5. ∀[n:ℤ]. (ml-select(n;v) ~ v[n])
6. n : ℤ
⊢ if n <z 1 then u else v[n - 1] fi  ~ let x,y = [u / v] 
                                       in if (n) < (1)  then x  else eval m = n - 1 in y[m]

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[L:T  List].  \mforall{}[n:\mBbbZ{}].    (ml-select(n;L)  \msim{}  L[n])  supposing  valueall-type(T)


By

---

Latex:
(InductionOnList
  THEN  (UnivCD  THENA  Auto)
  THEN  Unfold  `ml-select`  0
  THEN  (RW  (AddrC  [1]  (LemmaC  `ml\_apply-sq`))0  THEN  Auto)
  THEN  RW  (AddrC  [1;1]  (LemmaC  `ml\_apply-sq`))0
  THEN  Auto
  THEN  RW  (SweepUpC  UnrollRecursionC)  0
  THEN  Reduce  0
  THEN  Fold  `ml-select`  0
  THEN  Try  ((RecUnfold  `select`  0  THEN  (RWO  "-2"  0  THENA  Auto))))

---

Home Index