---

Step * 1 of Lemma mklist_add1


1. n : ℕ+
2. f : Top
⊢ mklist(n;f) ~ mklist(n - 1;f) @ [f (n - 1)]
BY
{ (Unfold `mklist` 0 THEN (RW  (AddrC [1] (LemmaC `primrec-unroll`)) 0 THENA Auto) THEN Reduce 0 THEN AutoSplit) }

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}\msupplus{}
2.  f  :  Top
\mvdash{}  mklist(n;f)  \msim{}  mklist(n  -  1;f)  @  [f  (n  -  1)]


By

---

Latex:
(Unfold  `mklist`  0
  THEN  (RW    (AddrC  [1]  (LemmaC  `primrec-unroll`))  0  THENA  Auto)
  THEN  Reduce  0
  THEN  AutoSplit)

---

Home Index