---

Step * of Lemma bag-member-iff-hd

∀[T:Type]. ∀[bs:bag(T)]. ∀[x:T].  uiff(x ↓∈ bs;↓∃L:T List. (bs = [x / L] ∈ bag(T)))
BY
{ (Auto THEN Auto) }

1
1. T : Type
2. bs : bag(T)
3. x : T
4. x ↓∈ bs
⊢ ↓∃L:T List. (bs = [x / L] ∈ bag(T))

2
1. T : Type
2. bs : bag(T)
3. x : T
4. ↓∃L:T List. (bs = [x / L] ∈ bag(T))
⊢ x ↓∈ bs

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[bs:bag(T)].  \mforall{}[x:T].    uiff(x  \mdownarrow{}\mmember{}  bs;\mdownarrow{}\mexists{}L:T  List.  (bs  =  [x  /  L]))


By

---

Latex:
(Auto  THEN  Auto)

---

Home Index