---

Step * 1 1 of Lemma ml-prodmap-sq


1. T : Type
2. A : Type
3. B : Type
4. valueall-type(T)
5. valueall-type(A)
6. valueall-type(B)
7. A
8. B
9. f : A ⟶ B ⟶ T
10. u : A
11. v : A List
12. ∀[bs:B List]. (ml-prodmap(f;v;bs) ~ eager-product-map(f;v;bs))
13. bs : B List
14. ↓∃:A. value-type(B ⟶ T)
⊢ ml-maprevappend(f(u);bs;eager-product-map(f;v;bs)) ~ eager-map-append(f u;bs;eager-product-map(f;v;bs))
BY
{ (RWO  "eager-map-append-sq ml-maprevappend-sq" 0 THEN EAuto 1) }

---

Latex:

---

Latex:

1.  T  :  Type
2.  A  :  Type
3.  B  :  Type
4.  valueall-type(T)
5.  valueall-type(A)
6.  valueall-type(B)
7.  A
8.  B
9.  f  :  A  {}\mrightarrow{}  B  {}\mrightarrow{}  T
10.  u  :  A
11.  v  :  A  List
12.  \mforall{}[bs:B  List].  (ml-prodmap(f;v;bs)  \msim{}  eager-product-map(f;v;bs))
13.  bs  :  B  List
14.  \mdownarrow{}\mexists{}:A.  value-type(B  {}\mrightarrow{}  T)
\mvdash{}  ml-maprevappend(f(u);bs;eager-product-map(f;v;bs)) 
\msim{}  eager-map-append(f  u;bs;eager-product-map(f;v;bs))


By

---

Latex:
(RWO    "eager-map-append-sq  ml-maprevappend-sq"  0  THEN  EAuto  1)

---

Home Index