---

Step * of Lemma bag-co-restrict-rep

∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[x:T]. ∀[n:ℕ].  ((bag-rep(n;x)|¬x) ~ {})
BY
{ ((PrimrecInductionOn `n' THENA Auto)
   THEN (RepUR ``bag-co-restrict`` 0 THEN Try (Trivial))
   THEN Try ((Fold `bag-co-restrict` 0 THEN AutoSplit))) }

---

Latex:

---

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


By

---

Latex:
((PrimrecInductionOn  `n'  THENA  Auto)
  THEN  (RepUR  ``bag-co-restrict``  0  THEN  Try  (Trivial))
  THEN  Try  ((Fold  `bag-co-restrict`  0  THEN  AutoSplit)))

---

Home Index