---

Step * of Lemma bag-rep-is-single-valued

∀[A:Type]. ∀[n:ℕ]. ∀[a:A].  single-valued-bag(bag-rep(n;a);A)
BY
{ (Unfold `single-valued-bag` 0 THEN Auto THEN RepeatFor 2 ((FLemma `member-bag-rep` [-2] THEN Auto))) }

---

Latex:

---

Latex:
\mforall{}[A:Type].  \mforall{}[n:\mBbbN{}].  \mforall{}[a:A].    single-valued-bag(bag-rep(n;a);A)


By

---

Latex:
(Unfold  `single-valued-bag`  0  THEN  Auto  THEN  RepeatFor  2  ((FLemma  `member-bag-rep`  [-2]  THEN  Auto)))

---

Home Index