---

Step * 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;ml-prodmap(f;v;bs)) ~ eager-map-append(f u;bs;eager-product-map(f;v;bs))
BY
{ ((RWO "-3" 0 THENA Auto) THEN RepUR ``let`` 0) }

1
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))

---

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;ml-prodmap(f;v;bs))  \msim{}  eager-map-append(f  u;bs;eager-product-map(f;v;bs))


By

---

Latex:
((RWO  "-3"  0  THENA  Auto)  THEN  RepUR  ``let``  0)

---

Home Index