---

Step * 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. b_all(A;v;x.↓∃y:B. P[x;y])
⇒ (↓∃bs:bag(A × B). ((bag-map(λx.(fst(x));bs) = v ∈ bag(A)) ∧ b_all(A × B;bs;x.let a,b = x in ↓P[a;b])))
7. b_all(A;[u / v];x.↓∃y:B. P[x;y])
⊢ ↓∃bs:bag(A × B). ((bag-map(λx.(fst(x));bs) = [u / v] ∈ bag(A)) ∧ b_all(A × B;bs;x.let a,b = x in ↓P[a;b]))
BY
{ (Fold `cons-bag` (-1) THEN (RWO "b_all-cons" (-1) THENA Auto) THEN RepD THEN (D (-3) THENA Auto) THEN SquashExRepD) }

1
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])
⊢ ↓∃bs:bag(A × B). ((bag-map(λx.(fst(x));bs) = [u / v] ∈ bag(A)) ∧ b_all(A × B;bs;x.let a,b = x in ↓P[a;b]))

---

Latex:

---

Latex:

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


By

---

Latex:
(Fold  `cons-bag`  (-1)
  THEN  (RWO  "b\_all-cons"  (-1)  THENA  Auto)
  THEN  RepD
  THEN  (D  (-3)  THENA  Auto)
  THEN  SquashExRepD)

---

Home Index