---

Step * of Lemma mklist-add

∀[T:Type]. ∀[n,m:ℕ]. ∀[f:ℕn + m ⟶ T].  (mklist(n + m;f) = (mklist(n;f) @ mklist(m;λi.(f (n + i)))) ∈ (T List))
BY
{ (Auto
   THEN (Assert λi.(f (n + i)) ∈ ℕm ⟶ T BY
               Auto')
   THEN (Assert f ∈ ℕn ⟶ T BY
               (ExtWith [`x'] [⌜ℕn + m ⟶ T⌝]⋅ THEN Auto'))
   THEN BLemma `list_extensionality`
   THEN Try (Complete (Auto'))) }

1
1. T : Type
2. n : ℕ
3. m : ℕ
4. f : ℕn + m ⟶ T
5. λi.(f (n + i)) ∈ ℕm ⟶ T
6. f ∈ ℕn ⟶ T
⊢ ∀i:ℕ. (i < ||mklist(n + m;f)|| ⇒ (mklist(n + m;f)[i] = mklist(n;f) @ mklist(m;λi.(f (n + i)))[i] ∈ T))

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[n,m:\mBbbN{}].  \mforall{}[f:\mBbbN{}n  +  m  {}\mrightarrow{}  T].    (mklist(n  +  m;f)  =  (mklist(n;f)  @  mklist(m;\mlambda{}i.(f  (n  +  i)))))


By

---

Latex:
(Auto
  THEN  (Assert  \mlambda{}i.(f  (n  +  i))  \mmember{}  \mBbbN{}m  {}\mrightarrow{}  T  BY
                          Auto')
  THEN  (Assert  f  \mmember{}  \mBbbN{}n  {}\mrightarrow{}  T  BY
                          (ExtWith  [`x']  [\mkleeneopen{}\mBbbN{}n  +  m  {}\mrightarrow{}  T\mkleeneclose{}]\mcdot{}  THEN  Auto'))
  THEN  BLemma  `list\_extensionality`
  THEN  Try  (Complete  (Auto')))

---

Home Index