---

Step * 2 of Lemma l_all_reduce


1. T : Type
2. u : T
3. v : T List
4. ∀[P:T ⟶ 𝔹]. uiff((∀x∈v.↑P[x]);↑reduce(λx,y. (P[x] ∧b y);tt;v))
⊢ ∀[P:T ⟶ 𝔹]. uiff((∀x∈[u / v].↑P[x]);↑(P[u] ∧b reduce(λx,y. (P[x] ∧b y);tt;v)))
BY
{ ((UnivCD THENA Auto) THEN (((RWO "l_all_cons" 0 THEN Auto) THEN All (RW assert_pushdownC)) THEN Auto) THEN Easy) }

---

Latex:

---

Latex:

1.  T  :  Type
2.  u  :  T
3.  v  :  T  List
4.  \mforall{}[P:T  {}\mrightarrow{}  \mBbbB{}].  uiff((\mforall{}x\mmember{}v.\muparrow{}P[x]);\muparrow{}reduce(\mlambda{}x,y.  (P[x]  \mwedge{}\msubb{}  y);tt;v))
\mvdash{}  \mforall{}[P:T  {}\mrightarrow{}  \mBbbB{}].  uiff((\mforall{}x\mmember{}[u  /  v].\muparrow{}P[x]);\muparrow{}(P[u]  \mwedge{}\msubb{}  reduce(\mlambda{}x,y.  (P[x]  \mwedge{}\msubb{}  y);tt;v)))


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  (((RWO  "l\_all\_cons"  0  THEN  Auto)  THEN  All  (RW  assert\_pushdownC))  THEN  Auto)
  THEN  Easy)

---

Home Index