---

Step * 1 1 of Lemma bag-member-append


1. T : Type
2. x : T
3. as : T List
4. bs : T List
5. L : T List
6. L = (as @ bs) ∈ bag(T)
7. (x ∈ L)
⊢ ↓x ↓∈ as ∨ x ↓∈ bs
BY
{ ((EqTypeD (-2) THENA Auto)
   THEN FLemma `member-permutation` [-2]
   THEN Auto
   THEN (FHyp (-1) [-2]⋅ THENA Auto)
   THEN RWO "member_append" (-1)
   THEN Auto
   THEN D 0
   THEN ParallelLast
   THEN Auto
   THEN D 0
   THEN Auto
   THEN Auto) }

---

Latex:

---

Latex:

1.  T  :  Type
2.  x  :  T
3.  as  :  T  List
4.  bs  :  T  List
5.  L  :  T  List
6.  L  =  (as  @  bs)
7.  (x  \mmember{}  L)
\mvdash{}  \mdownarrow{}x  \mdownarrow{}\mmember{}  as  \mvee{}  x  \mdownarrow{}\mmember{}  bs


By

---

Latex:
((EqTypeD  (-2)  THENA  Auto)
  THEN  FLemma  `member-permutation`  [-2]
  THEN  Auto
  THEN  (FHyp  (-1)  [-2]\mcdot{}  THENA  Auto)
  THEN  RWO  "member\_append"  (-1)
  THEN  Auto
  THEN  D  0
  THEN  ParallelLast
  THEN  Auto
  THEN  D  0
  THEN  Auto
  THEN  Auto)

---

Home Index