---

Step * 2 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. x1 : T
8. b = [x1] ∈ (T List)
⊢ x = y ∈ T
BY
{ (RWO "-1" (-3)
   THENA (Auto
          THEN RemoveLabel
          THEN EqTypeCD
          THEN Auto
          THEN HypSubst' (-1) 0
          THEN Auto
          THEN BLemma `permutation_weakening`
          THEN Auto)
   ) }

1
1. T : Type
2. b : T List
3. x : T
4. y : T
5. x ↓∈ b
6. x1 : T
7. b = [x1] ∈ (T List)
8. y ↓∈ [x1]
⊢ x = y ∈ T

---

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.  x1  :  T
8.  b  =  [x1]
\mvdash{}  x  =  y


By

---

Latex:
(RWO  "-1"  (-3)
  THENA  (Auto
                THEN  RemoveLabel
                THEN  EqTypeCD
                THEN  Auto
                THEN  HypSubst'  (-1)  0
                THEN  Auto
                THEN  BLemma  `permutation\_weakening`
                THEN  Auto)
  )

---

Home Index