---

Step * 1 of Lemma es-interface-vals-append


1. Info : Type
2. es : EO+(Info)
3. X : EClass(Top)
4. L1 : E(X) List
5. L2 : E(X) List
⊢ map(λe.X(e);L1 @ L2) ~ map(λe.X(e);L1) @ map(λe.X(e);L2)
BY
{ (RWO "map_append_sq" 0 THEN Auto)⋅ }

---

Latex:



1.  Info  :  Type
2.  es  :  EO+(Info)
3.  X  :  EClass(Top)
4.  L1  :  E(X)  List
5.  L2  :  E(X)  List
\mvdash{}  map(\mlambda{}e.X(e);L1  @  L2)  \msim{}  map(\mlambda{}e.X(e);L1)  @  map(\mlambda{}e.X(e);L2)


By

(RWO  "map\_append\_sq"  0  THEN  Auto)\mcdot{}

---

Home Index