---

Step * of Lemma select-repn

∀[x:Top]. ∀[n:ℕ]. ∀[i:ℕn].  (repn(n;x)[i] ~ x)
BY
{ (Unfold `repn` 0
   THEN InductionOnNat
   THEN Reduce 0
   THEN Auto
   THEN (RWO "primrec-unroll" 0 THENA Auto)
   THEN AutoSplit
   THEN (RWO "select-cons" 0 THENA Auto)
   THEN AutoSplit) }

---

Latex:

---

Latex:
\mforall{}[x:Top].  \mforall{}[n:\mBbbN{}].  \mforall{}[i:\mBbbN{}n].    (repn(n;x)[i]  \msim{}  x)


By

---

Latex:
(Unfold  `repn`  0
  THEN  InductionOnNat
  THEN  Reduce  0
  THEN  Auto
  THEN  (RWO  "primrec-unroll"  0  THENA  Auto)
  THEN  AutoSplit
  THEN  (RWO  "select-cons"  0  THENA  Auto)
  THEN  AutoSplit)

---

Home Index