---

Step * of Lemma assert-bag-all

∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[p:T ⟶ 𝔹]. ∀[bs:bag(T)].  (∀x:T. (x ↓∈ bs ⇒ (↑p[x])) ⇐⇒ ↑bag-all(x.p[x];bs))
BY
{ (Auto THEN (RWO "eqtt_to_assert<" 0⋅ THEN Auto)⋅) }

1
1. T : Type
2. eq : EqDecider(T)
3. p : T ⟶ 𝔹
4. bs : bag(T)
5. ∀x:T. (x ↓∈ bs ⇒ (↑p[x]))
⊢ bag-all(x.p[x];bs) = tt

2
1. T : Type
2. eq : EqDecider(T)
3. p : T ⟶ 𝔹
4. bs : bag(T)
5. ↑bag-all(x.p[x];bs)
6. x : T
7. x ↓∈ bs
⊢ p[x] = tt

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[eq:EqDecider(T)].  \mforall{}[p:T  {}\mrightarrow{}  \mBbbB{}].  \mforall{}[bs:bag(T)].
    (\mforall{}x:T.  (x  \mdownarrow{}\mmember{}  bs  {}\mRightarrow{}  (\muparrow{}p[x]))  \mLeftarrow{}{}\mRightarrow{}  \muparrow{}bag-all(x.p[x];bs))


By

---

Latex:
(Auto  THEN  (RWO  "eqtt\_to\_assert<"  0\mcdot{}  THEN  Auto)\mcdot{})

---

Home Index