---

Step * 2 1 1 1 of Lemma single-valued-bag-if-le1


1. T : Type
2. b : T List
3. x : T
4. y : T
5. x1 : T
6. b = [x1] ∈ (T List)
7. y ↓∈ [x1]
8. x ↓∈ [x1]
⊢ x = y ∈ T
BY
{ (All (Fold `single-bag`) THEN BagMemberD (-2) THEN BagMemberD (-1)⋅ THEN Eq) }

---

Latex:

---

Latex:

1.  T  :  Type
2.  b  :  T  List
3.  x  :  T
4.  y  :  T
5.  x1  :  T
6.  b  =  [x1]
7.  y  \mdownarrow{}\mmember{}  [x1]
8.  x  \mdownarrow{}\mmember{}  [x1]
\mvdash{}  x  =  y


By

---

Latex:
(All  (Fold  `single-bag`)  THEN  BagMemberD  (-2)  THEN  BagMemberD  (-1)\mcdot{}  THEN  Eq)

---

Home Index