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


1. Type
2. Type
3. 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 in ↓P[a;b]))
BY
(D THEN InstConcl [⌜[]⌝]⋅ THEN Auto THEN 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