---

Step * 2 1 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. x1 : T
7. b = [x1] ∈ (T List)
8. y ↓∈ [x1]
⊢ x = y ∈ T
BY
{ (RWO "-2" (-4)
   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. x1 : T
6. b = [x1] ∈ (T List)
7. y ↓∈ [x1]
8. x ↓∈ [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.  x1  :  T
7.  b  =  [x1]
8.  y  \mdownarrow{}\mmember{}  [x1]
\mvdash{}  x  =  y


By

---

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

---

Home Index