---

Step * 1 of Lemma bag-member-cons


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

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

---

Latex:

---

Latex:

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


By

---

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

---

Home Index