---

Step * 2 1 2 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])
12. bag-map(λx.(fst(x));<u, y>.bs) = [u / v] ∈ bag(A)
⊢ b_all(A × B;<u, y>.bs;x.let a,b = x 
            in ↓P[a;b])
BY
{ (BLemma `b_all-cons` THEN Reduce 0 THEN Auto THEN DProdsAndUnions THEN Reduce 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])
12.  bag-map(\mlambda{}x.(fst(x));<u,  y>.bs)  =  [u  /  v]
\mvdash{}  b\_all(A  \mtimes{}  B;<u,  y>.bs;x.let  a,b  =  x 
                        in  \mdownarrow{}P[a;b])


By

---

Latex:
(BLemma  `b\_all-cons`  THEN  Reduce  0  THEN  Auto  THEN  DProdsAndUnions  THEN  Reduce  0  THEN  Auto)

---

Home Index