---

Step * 1 1 of Lemma unzip-as-accum


1. u1 : Top
2. u2 : Top
3. v : (Top × Top) List
4. b1 : Top List
5. b2 : Top List
⊢ <b1 @ [u1 / map(λp.(fst(p));v)], b2 @ [u2 / map(λp.(snd(p));v)]> ~ <(b1 @ [u1]) @ map(λp.(fst(p));v)
                                                                   , (b2 @ [u2]) @ map(λp.(snd(p));v)
                                                                   >
BY
{ xxx((RWO "append_assoc_sq" 0 THENM Reduce 0) THEN Auto)xxx }

---

Latex:

---

Latex:

1.  u1  :  Top
2.  u2  :  Top
3.  v  :  (Top  \mtimes{}  Top)  List
4.  b1  :  Top  List
5.  b2  :  Top  List
\mvdash{}  <b1  @  [u1  /  map(\mlambda{}p.(fst(p));v)],  b2  @  [u2  /  map(\mlambda{}p.(snd(p));v)]>  \msim{}  <(b1  @  [u1])  @  map(\mlambda{}p.(fst(p));\000Cv)
                                                                                                                                      ,  (b2  @  [u2])
                                                                                                                                          @  map(\mlambda{}p.(snd(p));v)
                                                                                                                                      >


By

---

Latex:
xxx((RWO  "append\_assoc\_sq"  0  THENM  Reduce  0)  THEN  Auto)xxx

---

Home Index