---

Step * 1 2 of Lemma hd-map-spread


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]
BY
{ ((RWO "select-map" 0 THEN Auto) THEN Reduce 0 THEN Auto) }

---

Latex:

---

Latex:

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


By

---

Latex:
((RWO  "select-map"  0  THEN  Auto)  THEN  Reduce  0  THEN  Auto)

---

Home Index