---

Step * of Lemma eclass-union-classrel

∀[Info,A:Type]. ∀[X:EClass(bag(A))]. ∀[es:EO+(Info)]. ∀[e:E]. ∀[v:A].
  uiff(v ∈ eclass-union(X)(e);↓∃b:bag(A). (v ↓∈ b ∧ b ∈ X(e)))
BY
{ (Auto THEN All(RepUR ``eclass-union``)) }

1
1. Info : Type
2. A : Type
3. X : EClass(bag(A))
4. es : EO+(Info)
5. e : E
6. v : A
7. v ∈ λes,e. bag-union(X(e))(e)
⊢ ↓∃b:bag(A). (v ↓∈ b ∧ b ∈ X(e))

2
1. Info : Type
2. A : Type
3. X : EClass(bag(A))
4. es : EO+(Info)
5. e : E
6. v : A
7. ↓∃b:bag(A). (v ↓∈ b ∧ b ∈ X(e))
⊢ v ∈ λes,e. bag-union(X(e))(e)

---

Latex:

---

Latex:
\mforall{}[Info,A:Type].  \mforall{}[X:EClass(bag(A))].  \mforall{}[es:EO+(Info)].  \mforall{}[e:E].  \mforall{}[v:A].
    uiff(v  \mmember{}  eclass-union(X)(e);\mdownarrow{}\mexists{}b:bag(A).  (v  \mdownarrow{}\mmember{}  b  \mwedge{}  b  \mmember{}  X(e)))


By

---

Latex:
(Auto  THEN  All(RepUR  ``eclass-union``))

---

Home Index