---

Step * 1 1 of Lemma bag-member-union


1. T : Type
2. x : T
⊢ uiff(x ↓∈ bag-union([]);↓∃b:bag(T). (x ↓∈ b ∧ b ↓∈ []))
BY
{ (RepUR ``bag-union`` 0
   THEN Fold `empty-bag` 0
   THEN Auto
   THEN Try ((FLemma `bag-member-empty` [-1] THEN Auto))
   THEN Auto
   THEN D (-1)
   THEN Unhide
   THEN Auto
   THEN ExRepD
   THEN FLemma `bag-member-empty` [-1]
   THEN Auto) }

---

Latex:

---

Latex:

1.  T  :  Type
2.  x  :  T
\mvdash{}  uiff(x  \mdownarrow{}\mmember{}  bag-union([]);\mdownarrow{}\mexists{}b:bag(T).  (x  \mdownarrow{}\mmember{}  b  \mwedge{}  b  \mdownarrow{}\mmember{}  []))


By

---

Latex:
(RepUR  ``bag-union``  0
  THEN  Fold  `empty-bag`  0
  THEN  Auto
  THEN  Try  ((FLemma  `bag-member-empty`  [-1]  THEN  Auto))
  THEN  Auto
  THEN  D  (-1)
  THEN  Unhide
  THEN  Auto
  THEN  ExRepD
  THEN  FLemma  `bag-member-empty`  [-1]
  THEN  Auto)

---

Home Index