---

Step * 1 of Lemma cbv-concat-sq


1. u : Top List
2. v : Top List List
⊢ eval x = u in
  eval y = reduce(λl,l'. (l @ l');[];v) in
    x @ y ~ u @ reduce(λl,l'. (l @ l');[];v)
BY
{ RepeatFor 2 (CallByValueReduce 0
               THEN Auto) }

1
.....aux..... 
1. u : Top List
2. v : Top List List
⊢ (reduce(λl,l'. (l @ l');[];v))↓

---

Latex:

---

Latex:

1.  u  :  Top  List
2.  v  :  Top  List  List
\mvdash{}  eval  x  =  u  in
    eval  y  =  reduce(\mlambda{}l,l'.  (l  @  l');[];v)  in
        x  @  y  \msim{}  u  @  reduce(\mlambda{}l,l'.  (l  @  l');[];v)


By

---

Latex:
RepeatFor  2  (CallByValueReduce  0
                          THEN  Auto)

---

Home Index