---

Step * 2 1 of Lemma bag-member-cons


1. T : Type
2. x : T
3. u : T
4. L : T List
5. x = u ∈ T
⊢ x ↓∈ u.L
BY
{ ((HypSubst' (-1) 0 THENA Auto)
   THEN Unfold `bag-member` 0
   THEN D 0
   THEN (InstConcl [⌜[u / L]⌝]⋅ THENA Auto)
   THEN Unfold `cons-bag` 0
   THEN Auto) }

---

Latex:

---

Latex:

1.  T  :  Type
2.  x  :  T
3.  u  :  T
4.  L  :  T  List
5.  x  =  u
\mvdash{}  x  \mdownarrow{}\mmember{}  u.L


By

---

Latex:
((HypSubst'  (-1)  0  THENA  Auto)
  THEN  Unfold  `bag-member`  0
  THEN  D  0
  THEN  (InstConcl  [\mkleeneopen{}[u  /  L]\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  Unfold  `cons-bag`  0
  THEN  Auto)

---

Home Index