---

Step * of Lemma bag-co-restrict-disjoint

∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[x:T]. ∀[b:bag(T)].  (b|¬x) = b ∈ bag(T) supposing ¬x ↓∈ b
BY
{ xxx((Auto THEN BagToList 4) THEN Auto THEN RWO  "bag-member-list" (-1) THEN Auto)xxx }

1
1. T : Type
2. eq : EqDecider(T)
3. x : T
4. b : T List
5. ¬(x ∈ b)
⊢ (b|¬x) = b ∈ bag(T)

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[eq:EqDecider(T)].  \mforall{}[x:T].  \mforall{}[b:bag(T)].    (b|\mneg{}x)  =  b  supposing  \mneg{}x  \mdownarrow{}\mmember{}  b


By

---

Latex:
xxx((Auto  THEN  BagToList  4)  THEN  Auto  THEN  RWO    "bag-member-list"  (-1)  THEN  Auto)xxx

---

Home Index