---

Step * 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))
⊢ mklist-general(n - 1;h) @ [h mklist-general(n - 1;h)] ~ map(λn.mklist-general(n + 1;h)[n];upto(n - 1))
@ [(λn.mklist-general(n + 1;h)[n]) (n - 1)]
BY
{ (SqEqCD THEN Try (Complete (Auto))) }

1
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)] ~ [(λn.mklist-general(n + 1;h)[n]) (n - 1)]

---

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{}  mklist-general(n  -  1;h)  @  [h  mklist-general(n  -  1;h)] 
\msim{}  map(\mlambda{}n.mklist-general(n  +  1;h)[n];upto(n  -  1))  @  [(\mlambda{}n.mklist-general(n  +  1;h)[n])  (n  -  1)]


By

---

Latex:
(SqEqCD  THEN  Try  (Complete  (Auto)))

---

Home Index