---

Step * 2 of Lemma bag-member-cons


1. T : Type
2. x : T
3. u : T
4. v : bag(T)
5. ↓(x = u ∈ T) ∨ x ↓∈ v
⊢ x ↓∈ u.v
BY
{ (D (-1)
   THEN (Unhide THENA Auto)
   THEN (InstLemma `bag_to_squash_list` [⌜T⌝; ⌜v⌝]⋅ THENA Auto)
   THEN D (-1)
   THEN (Unhide THENA Auto)
   THEN D (-1)
   THEN (HypSubst' (-1) 0 THENA Auto)
   THEN (HypSubst' (-1) (-3) THENA Auto)
   THEN ThinVar `v'
   THEN D (-1)) }

1
1. T : Type
2. x : T
3. u : T
4. L : T List
5. x = u ∈ T
⊢ x ↓∈ u.L

2
1. T : Type
2. x : T
3. u : T
4. L : T List
5. x ↓∈ L
⊢ x ↓∈ u.L

---

Latex:

---

Latex:

1.  T  :  Type
2.  x  :  T
3.  u  :  T
4.  v  :  bag(T)
5.  \mdownarrow{}(x  =  u)  \mvee{}  x  \mdownarrow{}\mmember{}  v
\mvdash{}  x  \mdownarrow{}\mmember{}  u.v


By

---

Latex:
(D  (-1)
  THEN  (Unhide  THENA  Auto)
  THEN  (InstLemma  `bag\_to\_squash\_list`  [\mkleeneopen{}T\mkleeneclose{};  \mkleeneopen{}v\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  D  (-1)
  THEN  (Unhide  THENA  Auto)
  THEN  D  (-1)
  THEN  (HypSubst'  (-1)  0  THENA  Auto)
  THEN  (HypSubst'  (-1)  (-3)  THENA  Auto)
  THEN  ThinVar  `v'
  THEN  D  (-1))

---

Home Index