---

Step * of Lemma member-class-at

∀[Info,A:Type]. ∀[X:EClass(A)]. ∀[es:EO+(Info)]. ∀[e:E]. ∀[locs:bag(Id)].  uiff(↑e ∈b X@locs;(↑e ∈b X) ∧ loc(e) ↓∈ locs)
BY
{ ((UnivCD THENA Auto) THEN RepeatFor 2 ((D 0 THENA Auto))) }

1
1. Info : Type
2. A : Type
3. X : EClass(A)
4. es : EO+(Info)
5. e : E
6. locs : bag(Id)
7. ↑e ∈b X@locs
⊢ (↑e ∈b X) ∧ loc(e) ↓∈ locs

2
1. Info : Type
2. A : Type
3. X : EClass(A)
4. es : EO+(Info)
5. e : E
6. locs : bag(Id)
7. (↑e ∈b X) ∧ loc(e) ↓∈ locs
⊢ ↑e ∈b X@locs

---

Latex:

---

Latex:
\mforall{}[Info,A:Type].  \mforall{}[X:EClass(A)].  \mforall{}[es:EO+(Info)].  \mforall{}[e:E].  \mforall{}[locs:bag(Id)].
    uiff(\muparrow{}e  \mmember{}\msubb{}  X@locs;(\muparrow{}e  \mmember{}\msubb{}  X)  \mwedge{}  loc(e)  \mdownarrow{}\mmember{}  locs)


By

---

Latex:
((UnivCD  THENA  Auto)  THEN  RepeatFor  2  ((D  0  THENA  Auto)))

---

Home Index