---

Step * 2 of Lemma eager-product-map-nil


1. f : Top
2. u : Top
3. v : Top List
⊢ rec-case(v) of
  [] => []
  h::t =>
   r.r ~ []
BY
{ (ListInd (-1) THEN Reduce 0 THEN Auto) }

---

Latex:

---

Latex:

1.  f  :  Top
2.  u  :  Top
3.  v  :  Top  List
\mvdash{}  rec-case(v)  of
    []  =>  []
    h::t  =>
      r.r  \msim{}  []


By

---

Latex:
(ListInd  (-1)  THEN  Reduce  0  THEN  Auto)

---

Home Index