---

Step * 2 1 of Lemma assert-bag_all


1. T : Type
2. f : T ⟶ 𝔹
3. u : T
4. v : T List
5. ↑bag_all(v;f)
6. x : T
7. x ↓∈ u.v
8. ↑(f u)
9. ∀x:T. (x ↓∈ v ⇒ (↑(f x)))
⊢ ↑(f x)
BY
{ OnMaybeHyp 8 (\h. (BagMemberD h⋅ THEN D h THEN Auto THEN SplitOrHyps THEN Auto)) }

---

Latex:

---

Latex:

1.  T  :  Type
2.  f  :  T  {}\mrightarrow{}  \mBbbB{}
3.  u  :  T
4.  v  :  T  List
5.  \muparrow{}bag\_all(v;f)
6.  x  :  T
7.  x  \mdownarrow{}\mmember{}  u.v
8.  \muparrow{}(f  u)
9.  \mforall{}x:T.  (x  \mdownarrow{}\mmember{}  v  {}\mRightarrow{}  (\muparrow{}(f  x)))
\mvdash{}  \muparrow{}(f  x)


By

---

Latex:
OnMaybeHyp  8  (\mbackslash{}h.  (BagMemberD  h\mcdot{}  THEN  D  h  THEN  Auto  THEN  SplitOrHyps  THEN  Auto))

---

Home Index