---

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


1. T : Type
2. b : T List
3. x : T
4. y : T
5. x ↓∈ b
6. y ↓∈ b
7. ||b|| = 0 ∈ ℤ
⊢ x = y ∈ T
BY
{ ((RWO "length_zero" (-1) THENA Auto) THEN HypSubst' (-1) (-2) THEN Auto THEN BagMemberD (-2) THEN Auto) }

---

Latex:

---

Latex:

1.  T  :  Type
2.  b  :  T  List
3.  x  :  T
4.  y  :  T
5.  x  \mdownarrow{}\mmember{}  b
6.  y  \mdownarrow{}\mmember{}  b
7.  ||b||  =  0
\mvdash{}  x  =  y


By

---

Latex:
((RWO  "length\_zero"  (-1)  THENA  Auto)
  THEN  HypSubst'  (-1)  (-2)
  THEN  Auto
  THEN  BagMemberD  (-2)
  THEN  Auto)

---

Home Index