---

Step * of Lemma sub-bag-remove-if

∀[T:Type]. ∀[bs:bag(T)].  ∀eq:EqDecider(T). ∀as:bag(T). ∀x:T.  (sub-bag(T;as;bs) ⇒ sub-bag(T;as - x;bs))
BY
{ (Auto THEN All (Unfold `sub-bag`) THEN ExRepD THEN (Decide ↑bag-deq-member(eq;x;as) THENA Auto)) }

1
1. [T] : Type
2. [bs] : bag(T)
3. eq : EqDecider(T)
4. as : bag(T)
5. x : T
6. cs : bag(T)
7. bs = (as + cs) ∈ bag(T)
8. ↑bag-deq-member(eq;x;as)
⊢ ∃cs:bag(T). (bs = (as - x + cs) ∈ bag(T))

2
1. [T] : Type
2. [bs] : bag(T)
3. eq : EqDecider(T)
4. as : bag(T)
5. x : T
6. cs : bag(T)
7. bs = (as + cs) ∈ bag(T)
8. ¬↑bag-deq-member(eq;x;as)
⊢ ∃cs:bag(T). (bs = (as - x + cs) ∈ bag(T))

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[bs:bag(T)].
    \mforall{}eq:EqDecider(T).  \mforall{}as:bag(T).  \mforall{}x:T.    (sub-bag(T;as;bs)  {}\mRightarrow{}  sub-bag(T;as  -  x;bs))


By

---

Latex:
(Auto  THEN  All  (Unfold  `sub-bag`)  THEN  ExRepD  THEN  (Decide  \muparrow{}bag-deq-member(eq;x;as)  THENA  Auto))

---

Home Index