---

Step * 1 of Lemma fpf-accum_wf


1. A : Type
2. C : Type
3. B : A ⟶ Type
4. d : A List
5. x1 : a:{a:A| (a ∈ d)}  ⟶ B[a]
6. y : C
7. f : C ⟶ a:A ⟶ B[a] ⟶ C
⊢ accumulate (with value z and list item a):
   f[z;a;x1 a]
  over list:
    d
  with starting value:
   y) ∈ C
BY
{ xxx(AssertBY ⌜d ∈ {a:A| (a ∈ d)}  List⌝   (BLemma `list-subtype` THEN Auto)⋅ THEN Auto)xxx }

---

Latex:

---

Latex:

1.  A  :  Type
2.  C  :  Type
3.  B  :  A  {}\mrightarrow{}  Type
4.  d  :  A  List
5.  x1  :  a:\{a:A|  (a  \mmember{}  d)\}    {}\mrightarrow{}  B[a]
6.  y  :  C
7.  f  :  C  {}\mrightarrow{}  a:A  {}\mrightarrow{}  B[a]  {}\mrightarrow{}  C
\mvdash{}  accumulate  (with  value  z  and  list  item  a):
      f[z;a;x1  a]
    over  list:
        d
    with  starting  value:
      y)  \mmember{}  C


By

---

Latex:
xxx(AssertBY  \mkleeneopen{}d  \mmember{}  \{a:A|  (a  \mmember{}  d)\}    List\mkleeneclose{}      (BLemma  `list-subtype`  THEN  Auto)\mcdot{}  THEN  Auto)xxx

---

Home Index