---

Step * 1 1 of Lemma hd-map-spread


1. f : Top
⊢ map(λx.let a,b = x 
         in f[a;b];[])[0] ~ let a,b = [][0] 
                            in f[a;b]
BY
{ (Reduce 0 THEN Auto) }

---

Latex:

---

Latex:

1.  f  :  Top
\mvdash{}  map(\mlambda{}x.let  a,b  =  x 
                  in  f[a;b];[])[0]  \msim{}  let  a,b  =  [][0] 
                                                        in  f[a;b]


By

---

Latex:
(Reduce  0  THEN  Auto)

---

Home Index