---

Step * of Lemma bag-member-cons

∀[T:Type]. ∀[x,u:T]. ∀[v:bag(T)].  uiff(x ↓∈ u.v;(x = u ∈ T) ↓∨ x ↓∈ v)
BY
{ ((Unfold `sq_or` 0 THEN (UnivCD THENA Auto)) THEN (RepeatFor 2 (D 0) THENA Auto)) }

1
1. T : Type
2. x : T
3. u : T
4. v : bag(T)
5. x ↓∈ u.v
⊢ ↓(x = u ∈ T) ∨ x ↓∈ v

2
1. T : Type
2. x : T
3. u : T
4. v : bag(T)
5. ↓(x = u ∈ T) ∨ x ↓∈ v
⊢ x ↓∈ u.v

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[x,u:T].  \mforall{}[v:bag(T)].    uiff(x  \mdownarrow{}\mmember{}  u.v;(x  =  u)  \mdownarrow{}\mvee{}  x  \mdownarrow{}\mmember{}  v)


By

---

Latex:
((Unfold  `sq\_or`  0  THEN  (UnivCD  THENA  Auto))  THEN  (RepeatFor  2  (D  0)  THENA  Auto))

---

Home Index