---

Step * of Lemma single-valued-list-sv-bag

∀[A:Type]. ∀[L:A List].  single-valued-bag(L;A) supposing single-valued-list(L;A)
BY
{ (Auto THEN D 0 THEN Auto THEN Unfold `single-valued-list` 3 THEN BackThruSomeHyp THEN Fold `single-valued-list` 3) }

1
1. A : Type
2. L : A List
3. single-valued-list(L;A)
4. x : A@i
5. y : A@i
6. x ↓∈ L@i
7. y ↓∈ L@i
⊢ (x ∈ L)

2
1. A : Type
2. L : A List
3. single-valued-list(L;A)
4. x : A@i
5. y : A@i
6. x ↓∈ L@i
7. y ↓∈ L@i
⊢ (y ∈ L)

---

Latex:

---

Latex:
\mforall{}[A:Type].  \mforall{}[L:A  List].    single-valued-bag(L;A)  supposing  single-valued-list(L;A)


By

---

Latex:
(Auto
  THEN  D  0
  THEN  Auto
  THEN  Unfold  `single-valued-list`  3
  THEN  BackThruSomeHyp
  THEN  Fold  `single-valued-list`  3)

---

Home Index