---

Step * of Lemma eager-product-map-nil

∀[f:Top]. ∀[as:Top List].  (eager-product-map(f;as;[]) ~ [])
BY
{ (Auto THEN D -1 THEN RepUR ``eager-product-map`` 0) }

1
1. f : Top
⊢ [] ~ []

2
1. f : Top
2. u : Top
3. v : Top List
⊢ rec-case(v) of
  [] => []
  h::t =>
   r.r ~ []

---

Latex:

---

Latex:
\mforall{}[f:Top].  \mforall{}[as:Top  List].    (eager-product-map(f;as;[])  \msim{}  [])


By

---

Latex:
(Auto  THEN  D  -1  THEN  RepUR  ``eager-product-map``  0)

---

Home Index