---

Step * of Lemma eager_product_map_cons_lemma

∀L,as,a,f:Top.  (eager-product-map(f;[a / as];L) ~ eager-map-append(f a;L;eager-product-map(f;as;L)))
BY
{ (UnivCD THENA Auto) }

1
1. L : Top@i
2. as : Top@i
3. a : Top@i
4. f : Top@i
⊢ eager-product-map(f;[a / as];L) ~ eager-map-append(f a;L;eager-product-map(f;as;L))

---

Latex:

---

Latex:
\mforall{}L,as,a,f:Top.
    (eager-product-map(f;[a  /  as];L)  \msim{}  eager-map-append(f  a;L;eager-product-map(f;as;L)))


By

---

Latex:
(UnivCD  THENA  Auto)

---

Home Index