---

Step * 2 of Lemma bag-member-append


1. T : Type
2. x : T
3. as : T List
4. bs : T List
5. ↓x ↓∈ as ∨ x ↓∈ bs
⊢ x ↓∈ as @ bs
BY
{ (RepeatFor 3 ((D -1 THEN Try ((Unhide THEN Auto))))
   THEN ExRepD
   THEN ((EqTypeD (-2) THEN Auto)
         THEN FLemma `member-permutation` [-2]
         THEN Auto
         THEN FHyp (-1) [-2]
         THEN Auto
         THEN (D 0 THEN Auto)
         THEN With ⌜as @ bs⌝ (D 0)⋅
         THEN Auto)⋅) }

---

Latex:

---

Latex:

1.  T  :  Type
2.  x  :  T
3.  as  :  T  List
4.  bs  :  T  List
5.  \mdownarrow{}x  \mdownarrow{}\mmember{}  as  \mvee{}  x  \mdownarrow{}\mmember{}  bs
\mvdash{}  x  \mdownarrow{}\mmember{}  as  @  bs


By

---

Latex:
(RepeatFor  3  ((D  -1  THEN  Try  ((Unhide  THEN  Auto))))
  THEN  ExRepD
  THEN  ((EqTypeD  (-2)  THEN  Auto)
              THEN  FLemma  `member-permutation`  [-2]
              THEN  Auto
              THEN  FHyp  (-1)  [-2]
              THEN  Auto
              THEN  (D  0  THEN  Auto)
              THEN  With  \mkleeneopen{}as  @  bs\mkleeneclose{}  (D  0)\mcdot{}
              THEN  Auto)\mcdot{})

---

Home Index