---

Step * of Lemma b_all-inst

∀[B:Type]. ∀b:bag(B). ∀P:B ⟶ ℙ. ∀x:B.  (x ↓∈ b ⇒ b_all(B;b;x.P[x]) ⇒ P[x])
BY
{ Auto }

---

Latex:

---

Latex:
\mforall{}[B:Type].  \mforall{}b:bag(B).  \mforall{}P:B  {}\mrightarrow{}  \mBbbP{}.  \mforall{}x:B.    (x  \mdownarrow{}\mmember{}  b  {}\mRightarrow{}  b\_all(B;b;x.P[x])  {}\mRightarrow{}  P[x])


By

---

Latex:
Auto

---

Home Index