---

Step * of Lemma map_is_cons

∀[A,B:Type]. ∀[f:A ⟶ B]. ∀[L:A List]. ∀[L2:B List]. ∀[b:B].
  {((f hd(L)) = b ∈ B) ∧ (map(f;tl(L)) = L2 ∈ (B List))} supposing map(f;L) = [b / L2] ∈ (B List)
BY
{ (Auto THEN Unfold `guard` 0 THEN (InstLemma `map_is_append` [A; B; f; L; [b]; L2])⋅ THEN All Reduce THEN Auto) }

1
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

---

Latex:

---

Latex:
\mforall{}[A,B:Type].  \mforall{}[f:A  {}\mrightarrow{}  B].  \mforall{}[L:A  List].  \mforall{}[L2:B  List].  \mforall{}[b:B].
    \{((f  hd(L))  =  b)  \mwedge{}  (map(f;tl(L))  =  L2)\}  supposing  map(f;L)  =  [b  /  L2]


By

---

Latex:
(Auto
  THEN  Unfold  `guard`  0
  THEN  (InstLemma  `map\_is\_append`  [A;  B;  f;  L;  [b];  L2])\mcdot{}
  THEN  All  Reduce
  THEN  Auto)

---

Home Index