---

Step * of Lemma bag-subtract-member-if-no-repeats

∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[bs,as:bag(T)]. ∀[x:T].
  uiff(x ↓∈ bag-subtract(eq;bs;as);x ↓∈ bs ∧ (¬x ↓∈ as)) supposing bag-no-repeats(T;bs)
BY
{ (UnivCD THENA Auto) }

1
1. T : Type
2. eq : EqDecider(T)
3. bs : bag(T)
4. as : bag(T)
5. x : T
6. bag-no-repeats(T;bs)
⊢ uiff(x ↓∈ bag-subtract(eq;bs;as);x ↓∈ bs ∧ (¬x ↓∈ as))

---

Latex:

---

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


By

---

Latex:
(UnivCD  THENA  Auto)

---

Home Index