---

Step * 1 of Lemma mklist-general-length


1. h : Top
2. n : ℤ
3. n ≠ 0
4. 0 < n
5. ||mklist-general(n - 1;h)|| ~ n - 1
⊢ ||mklist-general(n - 1;h) @ [h mklist-general(n - 1;h)]|| ~ n
BY
{ ((RWO "length-append" 0⋅ THENA Auto) THEN HypSubst' (-1) 0 THEN Reduce 0 THEN Auto)⋅ }

---

Latex:

---

Latex:

1.  h  :  Top
2.  n  :  \mBbbZ{}
3.  n  \mneq{}  0
4.  0  <  n
5.  ||mklist-general(n  -  1;h)||  \msim{}  n  -  1
\mvdash{}  ||mklist-general(n  -  1;h)  @  [h  mklist-general(n  -  1;h)]||  \msim{}  n


By

---

Latex:
((RWO  "length-append"  0\mcdot{}  THENA  Auto)  THEN  HypSubst'  (-1)  0  THEN  Reduce  0  THEN  Auto)\mcdot{}

---

Home Index