---

Step * 1 of Lemma map_is_cons


1. A : Type
2. B : Type
3. f : A ⟶ B
4. L : A List
5. L2 : B List
6. b : B
7. map(f;L) = [b / L2] ∈ (B List)
8. map(f;firstn(1;L)) = [b] ∈ (B List)
9. map(f;nth_tl(1;L)) = L2 ∈ (B List)
⊢ (f hd(L)) = b ∈ B
BY
{ ((RecUnfold `firstn` (-2)) THEN D 4 THEN All Reduce THEN Obvious) }

---

Latex:

---

Latex:

1.  A  :  Type
2.  B  :  Type
3.  f  :  A  {}\mrightarrow{}  B
4.  L  :  A  List
5.  L2  :  B  List
6.  b  :  B
7.  map(f;L)  =  [b  /  L2]
8.  map(f;firstn(1;L))  =  [b]
9.  map(f;nth\_tl(1;L))  =  L2
\mvdash{}  (f  hd(L))  =  b


By

---

Latex:
((RecUnfold  `firstn`  (-2))  THEN  D  4  THEN  All  Reduce  THEN  Obvious)

---

Home Index