---

Step * 1 of Lemma hd-map-spread


1. f : Top
2. L : Top List
⊢ map(λx.let a,b = x 
         in f[a;b];L)[0] ~ let a,b = L[0] 
                           in f[a;b]
BY
{ D 2 }

1
1. f : Top
⊢ map(λx.let a,b = x 
         in f[a;b];[])[0] ~ let a,b = [][0] 
                            in f[a;b]

2
1. f : Top
2. u : Top
3. v : Top List
⊢ map(λx.let a,b = x 
         in f[a;b];[u / v])[0] ~ let a,b = [u / v][0] 
                                 in f[a;b]

---

Latex:

---

Latex:

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


By

---

Latex:
D  2

---

Home Index