---

Step * 2 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])
⊢ ↓∃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
{ (D 0 THEN InstConcl [⌜<u, y>.bs⌝]⋅ THEN Auto) }

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])
⊢ bag-map(λx.(fst(x));<u, y>.bs) = [u / v] ∈ bag(A)

2
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])

---

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{}  \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:
(D  0  THEN  InstConcl  [\mkleeneopen{}<u,  y>.bs\mkleeneclose{}]\mcdot{}  THEN  Auto)

---

Home Index