---

Step * 2 1 1 of Lemma b_all-squash-exists-bag


1. A : Type
2. B : Type
3. P : A ⟶ B ⟶ ℙ
4. u : A
5. v : A List
6. y : B
7. P[u;y]
8. b_all(A;v;x.↓∃y:B. P[x;y])
9. bs : bag(A × B)
10. bag-map(λx.(fst(x));bs) = v ∈ bag(A)
11. b_all(A × B;bs;x.let a,b = x 
                     in ↓P[a;b])
⊢ bag-map(λx.(fst(x));<u, y>.bs) = [u / v] ∈ bag(A)
BY
{ ((RWO "bag-map-cons" 0 THENA Auto) THEN Reduce 0 THEN Fold `cons-bag` 0 THEN RWO "-2" 0 THEN Auto) }

---

Latex:

---

Latex:

1.  A  :  Type
2.  B  :  Type
3.  P  :  A  {}\mrightarrow{}  B  {}\mrightarrow{}  \mBbbP{}
4.  u  :  A
5.  v  :  A  List
6.  y  :  B
7.  P[u;y]
8.  b\_all(A;v;x.\mdownarrow{}\mexists{}y:B.  P[x;y])
9.  bs  :  bag(A  \mtimes{}  B)
10.  bag-map(\mlambda{}x.(fst(x));bs)  =  v
11.  b\_all(A  \mtimes{}  B;bs;x.let  a,b  =  x 
                                          in  \mdownarrow{}P[a;b])
\mvdash{}  bag-map(\mlambda{}x.(fst(x));<u,  y>.bs)  =  [u  /  v]


By

---

Latex:
((RWO  "bag-map-cons"  0  THENA  Auto)  THEN  Reduce  0  THEN  Fold  `cons-bag`  0  THEN  RWO  "-2"  0  THEN  Auto)

---

Home Index