---

Step * 2 1 of Lemma eager-map-append-sq


1. T : Type
2. value-type(T)
3. A : Type
4. f : A ⟶ T
5. u : A
6. v : A List
7. ∀[bs:T List]. (eager-map-append(f;v;bs) ~ map(f;rev(v)) @ bs)
⊢ ∀[bs:T List]. (eager-map-append(f;v;eval x = f u in eval L' = bs in   [x / L']) ~ map(f;rev(v) @ [u]) @ bs)
BY
{ ((D 0 THENA Auto) THEN (RWO "7" 0 THENA Auto)) }

1
1. T : Type
2. value-type(T)
3. A : Type
4. f : A ⟶ T
5. u : A
6. v : A List
7. ∀[bs:T List]. (eager-map-append(f;v;bs) ~ map(f;rev(v)) @ bs)
8. bs : T List
⊢ map(f;rev(v)) @ eval x = f u in eval L' = bs in   [x / L'] ~ map(f;rev(v) @ [u]) @ bs

---

Latex:

---

Latex:

1.  T  :  Type
2.  value-type(T)
3.  A  :  Type
4.  f  :  A  {}\mrightarrow{}  T
5.  u  :  A
6.  v  :  A  List
7.  \mforall{}[bs:T  List].  (eager-map-append(f;v;bs)  \msim{}  map(f;rev(v))  @  bs)
\mvdash{}  \mforall{}[bs:T  List].  (eager-map-append(f;v;eval  x  =  f  u  in  eval  L'  =  bs  in      [x  /  L'])  \msim{}  map(f;rev(v)  @  [\000Cu])  @  bs)


By

---

Latex:
((D  0  THENA  Auto)  THEN  (RWO  "7"  0  THENA  Auto))

---

Home Index