---

Step * of Lemma mklist-general-fun

∀[T:Type]. ∀[h:(T List) ⟶ T]. ∀[n:ℕ].  (mklist-general(n;h) ~ map(λn.mklist-general(n + 1;h)[n];upto(n)))
BY
{ (Auto
   THEN NatInd (-1)
   THEN Try (Complete (((Subst ⌜upto(0) ~ []⌝ 0⋅ THENA Auto) THEN RepUR ``mklist-general map`` 0 THEN Auto)))) }

1
.....upcase..... 
1. T : Type
2. h : (T List) ⟶ T
3. n : ℤ
4. 0 < n
5. mklist-general(n - 1;h) ~ map(λn.mklist-general(n + 1;h)[n];upto(n - 1))
⊢ mklist-general(n;h) ~ map(λn.mklist-general(n + 1;h)[n];upto(n))

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[h:(T  List)  {}\mrightarrow{}  T].  \mforall{}[n:\mBbbN{}].
    (mklist-general(n;h)  \msim{}  map(\mlambda{}n.mklist-general(n  +  1;h)[n];upto(n)))


By

---

Latex:
(Auto
  THEN  NatInd  (-1)
  THEN  Try  (Complete  (((Subst  \mkleeneopen{}upto(0)  \msim{}  []\mkleeneclose{}  0\mcdot{}  THENA  Auto)
                                            THEN  RepUR  ``mklist-general  map``  0
                                            THEN  Auto))))

---

Home Index