---

Step * of Lemma mklist-general-add1

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

---

Latex:

---

Latex:
\mforall{}[n:\mBbbN{}].  \mforall{}[f:Top].    (mklist-general(n  +  1;f)  \msim{}  mklist-general(n;f)  @  [f  mklist-general(n;f)])


By

---

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

---

Home Index