---

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


1. A : Type
2. B : Type
3. P : A ⟶ B ⟶ ℙ
4. b_all(A;[];x.↓∃y:B. P[x;y])
⊢ ↓∃bs:bag(A × B). ((bag-map(λx.(fst(x));bs) = [] ∈ bag(A)) ∧ b_all(A × B;bs;x.let a,b = x in ↓P[a;b]))
BY
{ (D 0 THEN InstConcl [⌜[]⌝]⋅ THEN Auto THEN D 0 THEN Auto THEN BagMemberD (-1) THEN Auto) }

---

Latex:

---

Latex:

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


By

---

Latex:
(D  0  THEN  InstConcl  [\mkleeneopen{}[]\mkleeneclose{}]\mcdot{}  THEN  Auto  THEN  D  0  THEN  Auto  THEN  BagMemberD  (-1)  THEN  Auto)

---

Home Index