---

Step * of Lemma b_all-squash-exists-bag2

∀[A,B:Type]. ∀[as:bag(A)]. ∀[P:A ⟶ B ⟶ ℙ].
  ↓∃bs:bag(A × B). ((bag-map(λx.(fst(x));bs) = as ∈ bag(A)) ∧ b_all(A × B;bs;x.↓P[fst(x);snd(x)])) 
  supposing b_all(A;as;x.↓∃y:B. P[x;y])
BY
{ (Auto
   THEN (FLemma `b_all-squash-exists-bag` [-1] THENA Auto)
   THEN SquashExRepD
   THEN D 0
   THEN InstConcl [⌜bs⌝]⋅
   THEN Auto
   THEN RepeatFor 2 (ParallelOp -2)
   THEN ParallelLast
   THEN DProdsAndUnions
   THEN AllReduce
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[A,B:Type].  \mforall{}[as:bag(A)].  \mforall{}[P:A  {}\mrightarrow{}  B  {}\mrightarrow{}  \mBbbP{}].
    \mdownarrow{}\mexists{}bs:bag(A  \mtimes{}  B).  ((bag-map(\mlambda{}x.(fst(x));bs)  =  as)  \mwedge{}  b\_all(A  \mtimes{}  B;bs;x.\mdownarrow{}P[fst(x);snd(x)])) 
    supposing  b\_all(A;as;x.\mdownarrow{}\mexists{}y:B.  P[x;y])


By

---

Latex:
(Auto
  THEN  (FLemma  `b\_all-squash-exists-bag`  [-1]  THENA  Auto)
  THEN  SquashExRepD
  THEN  D  0
  THEN  InstConcl  [\mkleeneopen{}bs\mkleeneclose{}]\mcdot{}
  THEN  Auto
  THEN  RepeatFor  2  (ParallelOp  -2)
  THEN  ParallelLast
  THEN  DProdsAndUnions
  THEN  AllReduce
  THEN  Auto)

---

Home Index