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