---

Step * 2 of Lemma b_all-map2


1. [A] : Type
2. [B] : Type
3. b : bag(A)
4. f : {a:A| a ↓∈ b}  ⟶ B
5. P : B ⟶ ℙ
6. ∀b:B. SqStable(P[b])
7. b_all(A;b;x.P[f x])
⊢ b_all(B;bag-map(f;b);x.P[x])
BY
{ (All(RepUR ``b_all``)
   THEN (RWO "bag-member-map2" 0
         THENA (Try (Complete (Auto))
                THEN MemCD'
                THEN Try (Complete (Auto))
                THEN Using [`A',⌜{v:A| v ↓∈ b} ⌝] MemCD⋅
                THEN Auto
                THEN BLemma `bag-subtype`
                THEN Auto)
         )
   THEN Auto
   THEN TrySquashExRepD (-1)
   THEN InstHyp [⌜v⌝] (-4)⋅
   THEN Auto
   THEN DVarSets
   THEN Unhide
   THEN Auto) }

---

Latex:

---

Latex:

1.  [A]  :  Type
2.  [B]  :  Type
3.  b  :  bag(A)
4.  f  :  \{a:A|  a  \mdownarrow{}\mmember{}  b\}    {}\mrightarrow{}  B
5.  P  :  B  {}\mrightarrow{}  \mBbbP{}
6.  \mforall{}b:B.  SqStable(P[b])
7.  b\_all(A;b;x.P[f  x])
\mvdash{}  b\_all(B;bag-map(f;b);x.P[x])


By

---

Latex:
(All(RepUR  ``b\_all``)
  THEN  (RWO  "bag-member-map2"  0
              THENA  (Try  (Complete  (Auto))
                            THEN  MemCD'
                            THEN  Try  (Complete  (Auto))
                            THEN  Using  [`A',\mkleeneopen{}\{v:A|  v  \mdownarrow{}\mmember{}  b\}  \mkleeneclose{}]  MemCD\mcdot{}
                            THEN  Auto
                            THEN  BLemma  `bag-subtype`
                            THEN  Auto)
              )
  THEN  Auto
  THEN  TrySquashExRepD  (-1)
  THEN  InstHyp  [\mkleeneopen{}v\mkleeneclose{}]  (-4)\mcdot{}
  THEN  Auto
  THEN  DVarSets
  THEN  Unhide
  THEN  Auto)

---

Home Index