---

Step * of Lemma member-sub-bags

∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[bs,b:bag(T)].  uiff(b ↓∈ sub-bags(eq;bs);↓sub-bag(T;b;bs)) supposing valueall-type(T)
BY
{ xxxAutoxxx }

1
1. T : Type
2. valueall-type(T)
3. eq : EqDecider(T)
4. bs : bag(T)
5. b : bag(T)
6. b ↓∈ sub-bags(eq;bs)
⊢ ↓sub-bag(T;b;bs)

2
1. T : Type
2. valueall-type(T)
3. eq : EqDecider(T)
4. bs : bag(T)
5. b : bag(T)
6. ↓sub-bag(T;b;bs)
⊢ b ↓∈ sub-bags(eq;bs)

---

Latex:

---

Latex:
\mforall{}[T:Type]
    \mforall{}[eq:EqDecider(T)].  \mforall{}[bs,b:bag(T)].    uiff(b  \mdownarrow{}\mmember{}  sub-bags(eq;bs);\mdownarrow{}sub-bag(T;b;bs)) 
    supposing  valueall-type(T)


By

---

Latex:
xxxAutoxxx

---

Home Index