---

Step * 1 of Lemma hd-map


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

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

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

---

Latex:

---

Latex:

1.  f  :  Top
2.  L  :  Top  List
\mvdash{}  map(f;L)[0]  \msim{}  if  null(L)  then  \mbot{}  else  f  L[0]  fi 


By

---

Latex:
D  2

---

Home Index