---

Step * of Lemma hd-map-spread

∀[f:Top]. ∀[L:Top List].  (hd(map(λx.let a,b = x in f[a;b];L)) ~ let a,b = hd(L) in f[a;b])
BY
{ ((UnivCD THENA Auto) THEN (RWO "select0<" 0 THENA Auto)) }

1
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]

---

Latex:

---

Latex:
\mforall{}[f:Top].  \mforall{}[L:Top  List].    (hd(map(\mlambda{}x.let  a,b  =  x  in  f[a;b];L))  \msim{}  let  a,b  =  hd(L)  in  f[a;b])


By

---

Latex:
((UnivCD  THENA  Auto)  THEN  (RWO  "select0<"  0  THENA  Auto))

---

Home Index