---

Step * 2 2 of Lemma bag-member-cons


1. T : Type
2. x : T
3. u : T
4. L : T List
5. x ↓∈ L
⊢ x ↓∈ u.L
BY
{ (Unfold `bag-member` (-1)
   THEN Unfold `bag-member` 0
   THEN SquashExRepD
   THEN RenameVar `L0' (-3)
   THEN D 0
   THEN (RWO "-2<" 0 THENA Auto)
   THEN ThinVar `L'
   THEN (InstConcl [⌜[u / L0]⌝]⋅ 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  \mdownarrow{}\mmember{}  L
\mvdash{}  x  \mdownarrow{}\mmember{}  u.L


By

---

Latex:
(Unfold  `bag-member`  (-1)
  THEN  Unfold  `bag-member`  0
  THEN  SquashExRepD
  THEN  RenameVar  `L0'  (-3)
  THEN  D  0
  THEN  (RWO  "-2<"  0  THENA  Auto)
  THEN  ThinVar  `L'
  THEN  (InstConcl  [\mkleeneopen{}[u  /  L0]\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  Unfold  `cons-bag`  0
  THEN  Auto)

---

Home Index