---

Step * 1 of Lemma b_all-map2


1. [A] : Type
2. [B] : Type
3. b : bag(A)
4. f : {a:A| a ↓∈ b}  ⟶ B
5. P : B ⟶ ℙ
6. ∀b:B. SqStable(P[b])
7. b_all(B;bag-map(f;b);x.P[x])
⊢ b_all(A;b;x.P[f x])
BY
{ (ParallelLast
   THEN Auto
   THEN BackThruSomeHyp
   THEN BLemma `bag-member-map2`
   THEN Auto
   THEN D 0
   THEN D 0 With ⌜x⌝ 
   THEN Auto) }

---

Latex:

---

Latex:

1.  [A]  :  Type
2.  [B]  :  Type
3.  b  :  bag(A)
4.  f  :  \{a:A|  a  \mdownarrow{}\mmember{}  b\}    {}\mrightarrow{}  B
5.  P  :  B  {}\mrightarrow{}  \mBbbP{}
6.  \mforall{}b:B.  SqStable(P[b])
7.  b\_all(B;bag-map(f;b);x.P[x])
\mvdash{}  b\_all(A;b;x.P[f  x])


By

---

Latex:
(ParallelLast
  THEN  Auto
  THEN  BackThruSomeHyp
  THEN  BLemma  `bag-member-map2`
  THEN  Auto
  THEN  D  0
  THEN  D  0  With  \mkleeneopen{}x\mkleeneclose{} 
  THEN  Auto)

---

Home Index