---

Step * of Lemma super-fact-unroll

∀[n:ℕ+]. ((n)!! ~ (n)! * (n - 1)!!)
BY
{ (Auto
   THEN RW (AddrC [2] UnfoldTopAbC) 0
   THEN (RWO "primrec-unroll" 0 THENA Auto)
   THEN Reduce 0
   THEN Fold `super-fact` 0
   THEN AutoSplit) }

---

Latex:

---

Latex:
\mforall{}[n:\mBbbN{}\msupplus{}].  ((n)!!  \msim{}  (n)!  *  (n  -  1)!!)


By

---

Latex:
(Auto
  THEN  RW  (AddrC  [2]  UnfoldTopAbC)  0
  THEN  (RWO  "primrec-unroll"  0  THENA  Auto)
  THEN  Reduce  0
  THEN  Fold  `super-fact`  0
  THEN  AutoSplit)

---

Home Index