---

Step * 1 of Lemma mklist-add1


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

---

Latex:

---

Latex:

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


By

---

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

---

Home Index