---

Step * 1 of Lemma bl-all-as-accum


1. T : Type
2. L : T List
3. P : T ⟶ 𝔹
⊢ accumulate (with value p and list item x):
   P[x] ∧b p
  over list:
    L
  with starting value:
   tt) 
= accumulate (with value p and list item x):
   p ∧b P[x]
  over list:
    L
  with starting value:
   tt)
BY
{ (EqCD THEN Auto) }

---

Latex:

---

Latex:

1.  T  :  Type
2.  L  :  T  List
3.  P  :  T  {}\mrightarrow{}  \mBbbB{}
\mvdash{}  accumulate  (with  value  p  and  list  item  x):
      P[x]  \mwedge{}\msubb{}  p
    over  list:
        L
    with  starting  value:
      tt) 
=  accumulate  (with  value  p  and  list  item  x):
      p  \mwedge{}\msubb{}  P[x]
    over  list:
        L
    with  starting  value:
      tt)


By

---

Latex:
(EqCD  THEN  Auto)

---

Home Index