---

Step * 1 1 2 of Lemma ml-maprevappend-sq


1. T : Type
2. A : Type
3. f : A ⟶ T
4. valueall-type(T)
5. valueall-type(A)
6. A
7. valueall-type(A ⟶ T)
8. u : A
9. v : A List
10. ∀bs:T List. (ml-maprevappend(f;v;bs) ~ map(f;rev(v)) @ bs)
11. bs : T List
12. ml-maprevappend(f;v;[f u / bs]) ~ map(f;rev(v)) @ [f u / bs]
⊢ map(f;rev([u / v])) @ bs ~ map(f;rev(v)) @ [f u / bs]
BY
{ ((RWW  "reverse-cons map_append_sq append_assoc" 0 THENA Auto) THEN Reduce 0 THEN Auto) }

---

Latex:

---

Latex:

1.  T  :  Type
2.  A  :  Type
3.  f  :  A  {}\mrightarrow{}  T
4.  valueall-type(T)
5.  valueall-type(A)
6.  A
7.  valueall-type(A  {}\mrightarrow{}  T)
8.  u  :  A
9.  v  :  A  List
10.  \mforall{}bs:T  List.  (ml-maprevappend(f;v;bs)  \msim{}  map(f;rev(v))  @  bs)
11.  bs  :  T  List
12.  ml-maprevappend(f;v;[f  u  /  bs])  \msim{}  map(f;rev(v))  @  [f  u  /  bs]
\mvdash{}  map(f;rev([u  /  v]))  @  bs  \msim{}  map(f;rev(v))  @  [f  u  /  bs]


By

---

Latex:
((RWW    "reverse-cons  map\_append\_sq  append\_assoc"  0  THENA  Auto)  THEN  Reduce  0  THEN  Auto)

---

Home Index