---

Step * of Lemma bag-subtract-no-repeats

∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[bs,as:bag(T)].  bag-no-repeats(T;bag-subtract(eq;bs;as)) supposing bag-no-repeats(T;bs)
BY
{ Auto }

1
1. T : Type
2. eq : EqDecider(T)
3. bs : bag(T)
4. as : bag(T)
5. bag-no-repeats(T;bs)
⊢ bag-no-repeats(T;bag-subtract(eq;bs;as))

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[eq:EqDecider(T)].  \mforall{}[bs,as:bag(T)].
    bag-no-repeats(T;bag-subtract(eq;bs;as))  supposing  bag-no-repeats(T;bs)


By

---

Latex:
Auto

---

Home Index