---

Step * of Lemma hd-map

∀[f:Top]. ∀[L:Top List].  (hd(map(f;L)) ~ if null(L) then ⊥ else f hd(L) fi )
BY
{ ((UnivCD THENA Auto) THEN (RWO "select0<" 0 THENA Auto)) }

1
1. f : Top
2. L : Top List
⊢ map(f;L)[0] ~ if null(L) then ⊥ else f L[0] fi 

---

Latex:

---

Latex:
\mforall{}[f:Top].  \mforall{}[L:Top  List].    (hd(map(f;L))  \msim{}  if  null(L)  then  \mbot{}  else  f  hd(L)  fi  )


By

---

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

---

Home Index