---

Step * of Lemma mklist-prepend1

∀[f:Top]. ∀[m:ℕ].  (mklist(1 + m;f) ~ [f 0] @ mklist(m;λi.(f (1 + i))))
BY
{ ((UnivCD THENA Auto) THEN NatInd (-1) THEN Reduce 0 THEN Auto THEN (Subst ⌜1 + (m - 1) ~ m⌝ (-1)⋅ THENA Auto)) }

1
1. f : Top
2. m : ℤ
3. 0 < m
4. mklist(m;f) ~ [f 0] @ mklist(m - 1;λi.(f (1 + i)))
⊢ mklist(1 + m;f) ~ [f 0 / mklist(m;λi.(f (1 + i)))]

---

Latex:

---

Latex:
\mforall{}[f:Top].  \mforall{}[m:\mBbbN{}].    (mklist(1  +  m;f)  \msim{}  [f  0]  @  mklist(m;\mlambda{}i.(f  (1  +  i))))


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  NatInd  (-1)
  THEN  Reduce  0
  THEN  Auto
  THEN  (Subst  \mkleeneopen{}1  +  (m  -  1)  \msim{}  m\mkleeneclose{}  (-1)\mcdot{}  THENA  Auto))

---

Home Index