---

Step * 2 1 1 1 1 1 1 of Lemma bag-member-splits


1. T : Type
2. as : T List
3. bs : T List
4. permutation(T;[];as @ bs)
⊢ (<as, bs> ∈ {<{}, {}>})
BY
{ ((RWO "permutation-nil-iff" (-1) THENA Auto) THEN AutoSimpHyp Auto (-1) THEN RepUR ``single-bag empty-bag`` 0)⋅ }

1
1. T : Type
2. as : T List
3. bs : T List
4. as = [] ∈ (T List)
5. bs = [] ∈ (T List)
⊢ (<as, bs> ∈ [<[], []>])

---

Latex:

---

Latex:

1.  T  :  Type
2.  as  :  T  List
3.  bs  :  T  List
4.  permutation(T;[];as  @  bs)
\mvdash{}  (<as,  bs>  \mmember{}  \{<\{\},  \{\}>\})


By

---

Latex:
((RWO  "permutation-nil-iff"  (-1)  THENA  Auto)
  THEN  AutoSimpHyp  Auto  (-1)
  THEN  RepUR  ``single-bag  empty-bag``  0)\mcdot{}

---

Home Index