---

Step * 1 1 of Lemma bag-member-cons


1. T : Type
2. x : T
3. u : T
4. L : T List
5. x ↓∈ u.L
⊢ ↓(x = u ∈ T) ∨ x ↓∈ L
BY
{ (Unfold `cons-bag` (-1)
   THEN (Subst ⌜[u / L] ~ [u] @ L⌝ (-1)⋅ THENA (RepUR ``append`` 0 THEN Auto))
   THEN Try (Fold `bag-append` (-1)⋅)
   THEN (FLemma `bag-member-append` [-1] THENA Auto)
   THEN D (-1)
   THEN Try (Fold `single-bag` (-1))
   THEN D (-1)) }

1
1. T : Type
2. x : T
3. u : T
4. L : T List
5. x ↓∈ [u] + L
6. x ↓∈ {u}
⊢ ↓(x = u ∈ T) ∨ x ↓∈ L

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

---

Latex:

---

Latex:

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


By

---

Latex:
(Unfold  `cons-bag`  (-1)
  THEN  (Subst  \mkleeneopen{}[u  /  L]  \msim{}  [u]  @  L\mkleeneclose{}  (-1)\mcdot{}  THENA  (RepUR  ``append``  0  THEN  Auto))
  THEN  Try  (Fold  `bag-append`  (-1)\mcdot{})
  THEN  (FLemma  `bag-member-append`  [-1]  THENA  Auto)
  THEN  D  (-1)
  THEN  Try  (Fold  `single-bag`  (-1))
  THEN  D  (-1))

---

Home Index