---

Step * of Lemma bag-in-subtype

∀[A,B:Type].  ∀[b:bag(B)]. b ∈ bag(A) supposing ∀x:B. (x ↓∈ b ⇒ (x ∈ A)) supposing strong-subtype(A;B)
BY
{ (RepeatFor 4 (Intro)
   THEN (Assert respects-equality(B;A) BY
               ((Unhide THENA Auto) THEN RWO  "strong-subtype-iff-respects-equality" (-2)⋅ THEN Auto))
   THEN (Assert respects-equality(bag(B);bag(A)) BY
               EAuto 1)
   THEN (InstLemma `equal-wf` [⌜B⌝;⌜B⌝;⌜A⌝]⋅ THENA Auto)
   THEN (InstLemma `equal-wf` [⌜bag(B)⌝;⌜bag(B)⌝;⌜bag(A)⌝]⋅ THENA Auto)
   THEN Intro
   THEN Unhide) }

1
1. A : Type
2. B : Type
3. strong-subtype(A;B)
4. b : bag(B)
5. respects-equality(B;A)
6. respects-equality(bag(B);bag(A))
7. ∀[a,b:B].  (a = b ∈ A ∈ ℙ)
8. ∀[a,b:bag(B)].  (a = b ∈ bag(A) ∈ ℙ)
9. ∀x:B. (x ↓∈ b ⇒ (x ∈ A))
⊢ b ∈ bag(A)

---

Latex:

---

Latex:
\mforall{}[A,B:Type].
    \mforall{}[b:bag(B)].  b  \mmember{}  bag(A)  supposing  \mforall{}x:B.  (x  \mdownarrow{}\mmember{}  b  {}\mRightarrow{}  (x  \mmember{}  A))  supposing  strong-subtype(A;B)


By

---

Latex:
(RepeatFor  4  (Intro)
  THEN  (Assert  respects-equality(B;A)  BY
                          ((Unhide  THENA  Auto)  THEN  RWO    "strong-subtype-iff-respects-equality"  (-2)\mcdot{}  THEN  Auto))
  THEN  (Assert  respects-equality(bag(B);bag(A))  BY
                          EAuto  1)
  THEN  (InstLemma  `equal-wf`  [\mkleeneopen{}B\mkleeneclose{};\mkleeneopen{}B\mkleeneclose{};\mkleeneopen{}A\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (InstLemma  `equal-wf`  [\mkleeneopen{}bag(B)\mkleeneclose{};\mkleeneopen{}bag(B)\mkleeneclose{};\mkleeneopen{}bag(A)\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  Intro
  THEN  Unhide)

---

Home Index