---

Step * of Lemma bag-restrict-rep

∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[x:T]. ∀[n:ℕ].  ((bag-rep(n;x)|x) ~ bag-rep(n;x))
BY
{ (RepUR ``bag-restrict bag-rep empty-bag bag-filter cons-bag`` 0
   THEN InductionOnNat
   THEN Auto
   THEN Reduce 0
   THEN Auto
   THEN (RWO "primrec-unroll" 0 THENA Auto)
   THEN RepeatFor 2 (AutoSplit)) }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[eq:EqDecider(T)].  \mforall{}[x:T].  \mforall{}[n:\mBbbN{}].    ((bag-rep(n;x)|x)  \msim{}  bag-rep(n;x))


By

---

Latex:
(RepUR  ``bag-restrict  bag-rep  empty-bag  bag-filter  cons-bag``  0
  THEN  InductionOnNat
  THEN  Auto
  THEN  Reduce  0
  THEN  Auto
  THEN  (RWO  "primrec-unroll"  0  THENA  Auto)
  THEN  RepeatFor  2  (AutoSplit))

---

Home Index