---

Step * 2 1 1 of Lemma assert-bag-all


∀L:𝔹 List. ((↑reduce(λx,y. (x ∧b y);tt;L)) ⇒ (∀b:𝔹. ((b ∈ L) ⇒ b = tt)))
BY
{ (InductionOnList THEN Reduce 0) }

1
True ⇒ (∀b:𝔹. ((b ∈ []) ⇒ b = tt))

2
1. u : 𝔹
2. v : 𝔹 List
3. (↑reduce(λx,y. (x ∧b y);tt;v)) ⇒ (∀b:𝔹. ((b ∈ v) ⇒ b = tt))
⊢ (↑(u ∧b reduce(λx,y. (x ∧b y);tt;v))) ⇒ (∀b:𝔹. ((b ∈ [u / v]) ⇒ b = tt))

---

Latex:

---

Latex:

\mforall{}L:\mBbbB{}  List.  ((\muparrow{}reduce(\mlambda{}x,y.  (x  \mwedge{}\msubb{}  y);tt;L))  {}\mRightarrow{}  (\mforall{}b:\mBbbB{}.  ((b  \mmember{}  L)  {}\mRightarrow{}  b  =  tt)))


By

---

Latex:
(InductionOnList  THEN  Reduce  0)

---

Home Index