---

Step * 2 of Lemma sub-bag-no-repeats-iff


1. T : Type
2. eq : EqDecider(T)
3. b1 : bag(T)
4. b2 : bag(T)
5. bag-no-repeats(T;b1)
6. sub-bag(T;b1;b2)
7. x : T
8. x ↓∈ b1
⊢ x ↓∈ b2
BY
{ (Unfold `sub-bag` (-3)
   THEN ExRepD
   THEN (HypSubst' (-3) 0 THENA Auto)
   THEN (RWO "bag-member-append" 0 THENA Auto)
   THEN (D 0 THEN Auto)
   THEN OrLeft
   THEN Auto) }

---

Latex:

---

Latex:

1.  T  :  Type
2.  eq  :  EqDecider(T)
3.  b1  :  bag(T)
4.  b2  :  bag(T)
5.  bag-no-repeats(T;b1)
6.  sub-bag(T;b1;b2)
7.  x  :  T
8.  x  \mdownarrow{}\mmember{}  b1
\mvdash{}  x  \mdownarrow{}\mmember{}  b2


By

---

Latex:
(Unfold  `sub-bag`  (-3)
  THEN  ExRepD
  THEN  (HypSubst'  (-3)  0  THENA  Auto)
  THEN  (RWO  "bag-member-append"  0  THENA  Auto)
  THEN  (D  0  THEN  Auto)
  THEN  OrLeft
  THEN  Auto)

---

Home Index