---

Step * 2 1 of Lemma bag-member-single


1. T : Type
2. x : T
3. y : T
4. x = y ∈ T
⊢ y ↓∈ {y}
BY
{ ((D 0 THEN Auto) THEN With ⌜[y]⌝ (D 0)⋅ THEN Auto THEN Fold `single-bag` 0 THEN Auto) }

---

Latex:

---

Latex:

1.  T  :  Type
2.  x  :  T
3.  y  :  T
4.  x  =  y
\mvdash{}  y  \mdownarrow{}\mmember{}  \{y\}


By

---

Latex:
((D  0  THEN  Auto)  THEN  With  \mkleeneopen{}[y]\mkleeneclose{}  (D  0)\mcdot{}  THEN  Auto  THEN  Fold  `single-bag`  0  THEN  Auto)

---

Home Index