---

Step * of Lemma b_all-squash-exists-bag

∀[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.let a,b = x in ↓P[a;b])) 
  supposing b_all(A;as;x.↓∃y:B. P[x;y])
BY
{ (Auto THEN (BagToList (-3) THENA Auto) THEN ListInd (-3) THEN (D 0 THENA Auto)) }

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

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

---

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.let  a,b  =  x  in  \mdownarrow{}P[a;b])) 
    supposing  b\_all(A;as;x.\mdownarrow{}\mexists{}y:B.  P[x;y])


By

---

Latex:
(Auto  THEN  (BagToList  (-3)  THENA  Auto)  THEN  ListInd  (-3)  THEN  (D  0  THENA  Auto))

---

Home Index