---

Step * 1 of Lemma b_all-map


1. [A] : Type
2. [B] : Type
3. f : A ⟶ B
4. b : bag(A)
5. P : B ⟶ ℙ
6. ∀b:B. SqStable(P[b])
7. ∀x:A. (x ↓∈ b ⇒ P[f x])
8. x : B
9. ↓∃v:A. (v ↓∈ b ∧ (x = (f v) ∈ B))
⊢ P[x]
BY
{ (TrySquashExRepD (-1) THEN InstHyp [⌜v⌝] (-5)⋅ THEN Auto) }

---

Latex:

---

Latex:

1.  [A]  :  Type
2.  [B]  :  Type
3.  f  :  A  {}\mrightarrow{}  B
4.  b  :  bag(A)
5.  P  :  B  {}\mrightarrow{}  \mBbbP{}
6.  \mforall{}b:B.  SqStable(P[b])
7.  \mforall{}x:A.  (x  \mdownarrow{}\mmember{}  b  {}\mRightarrow{}  P[f  x])
8.  x  :  B
9.  \mdownarrow{}\mexists{}v:A.  (v  \mdownarrow{}\mmember{}  b  \mwedge{}  (x  =  (f  v)))
\mvdash{}  P[x]


By

---

Latex:
(TrySquashExRepD  (-1)  THEN  InstHyp  [\mkleeneopen{}v\mkleeneclose{}]  (-5)\mcdot{}  THEN  Auto)

---

Home Index