---

Step * of Lemma bag-member-subtype

∀[A,B:Type].  ∀b:bag(A). ∀x:A.  (x ↓∈ b ⇒ x ↓∈ b) supposing A ⊆r B
BY
{ (Auto
   THEN BagToList 4
   THEN Auto
   THEN Unfold `bag-member` (-1)
   THEN (TrySquashExRepD (-1) THENA Auto)
   THEN (RevHypSubst' (-2) 0 THENA Auto)
   THEN ThinVar `b'
   THEN Unfold `bag-member` 0
   THEN D 0
   THEN InstConcl [⌜L⌝]⋅
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[A,B:Type].    \mforall{}b:bag(A).  \mforall{}x:A.    (x  \mdownarrow{}\mmember{}  b  {}\mRightarrow{}  x  \mdownarrow{}\mmember{}  b)  supposing  A  \msubseteq{}r  B


By

---

Latex:
(Auto
  THEN  BagToList  4
  THEN  Auto
  THEN  Unfold  `bag-member`  (-1)
  THEN  (TrySquashExRepD  (-1)  THENA  Auto)
  THEN  (RevHypSubst'  (-2)  0  THENA  Auto)
  THEN  ThinVar  `b'
  THEN  Unfold  `bag-member`  0
  THEN  D  0
  THEN  InstConcl  [\mkleeneopen{}L\mkleeneclose{}]\mcdot{}
  THEN  Auto)

---

Home Index