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