---

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


1. T : Type
2. p : T ⟶ 𝔹
3. x : T
4. as : T List
⊢ (x ∈ as) ⇒ (↑reduce(λx,y. (x ∧b y);tt;map(λx.p[x];as))) ⇒ p[x] = tt
BY
{ (ListInd (-1) THEN Reduce 0 THEN Auto)⋅ }

1
1. T : Type
2. p : T ⟶ 𝔹
3. x : T
4. u : T
5. v : T List
6. (x ∈ v) ⇒ (↑reduce(λx,y. (x ∧b y);tt;map(λx.p[x];v))) ⇒ p[x] = tt
7. (x ∈ [u / v])
8. ↑(p[u] ∧b reduce(λx,y. (x ∧b y);tt;map(λx.p[x];v)))
⊢ p[x] = tt

---

Latex:

---

Latex:

1.  T  :  Type
2.  p  :  T  {}\mrightarrow{}  \mBbbB{}
3.  x  :  T
4.  as  :  T  List
\mvdash{}  (x  \mmember{}  as)  {}\mRightarrow{}  (\muparrow{}reduce(\mlambda{}x,y.  (x  \mwedge{}\msubb{}  y);tt;map(\mlambda{}x.p[x];as)))  {}\mRightarrow{}  p[x]  =  tt


By

---

Latex:
(ListInd  (-1)  THEN  Reduce  0  THEN  Auto)\mcdot{}

---

Home Index