---

Step * 1 1 1 1 1 of Lemma mklist-general-fun


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))
6. hide : Base
7. hide ~ λn,h. map(λn.mklist-general(n + 1;h)[n];upto(n))
⊢ [h mklist-general(n - 1;h)] ~ [last(mklist-general(n;h))]
BY
{ ((Subst ⌜mklist-general(n;h) ~ mklist-general(n - 1;h) @ [h mklist-general(n - 1;h)]⌝ 0⋅
    THENA (BLemma `mklist-general_add1`  THEN Auto)
    )
   THEN RWO "last_append_singleton" 0
   THEN Auto) }

---

Latex:

---

Latex:

1.  T  :  Type
2.  h  :  (T  List)  {}\mrightarrow{}  T
3.  n  :  \mBbbZ{}
4.  0  <  n
5.  mklist-general(n  -  1;h)  \msim{}  map(\mlambda{}n.mklist-general(n  +  1;h)[n];upto(n  -  1))
6.  hide  :  Base
7.  hide  \msim{}  \mlambda{}n,h.  map(\mlambda{}n.mklist-general(n  +  1;h)[n];upto(n))
\mvdash{}  [h  mklist-general(n  -  1;h)]  \msim{}  [last(mklist-general(n;h))]


By

---

Latex:
((Subst  \mkleeneopen{}mklist-general(n;h)  \msim{}  mklist-general(n  -  1;h)  @  [h  mklist-general(n  -  1;h)]\mkleeneclose{}  0\mcdot{}
    THENA  (BLemma  `mklist-general\_add1`    THEN  Auto)
    )
  THEN  RWO  "last\_append\_singleton"  0
  THEN  Auto)

---

Home Index