---

Step * 1 1 of Lemma cbv-concat-sq

.....aux..... 
1. u : Top List
2. v : Top List List
⊢ (reduce(λl,l'. (l @ l');[];v))↓
BY
{ (GenConclAtAddrType ⌜Top List⌝ [1]⋅ THEN Auto) }

---

Latex:

---

Latex:
.....aux..... 
1.  u  :  Top  List
2.  v  :  Top  List  List
\mvdash{}  (reduce(\mlambda{}l,l'.  (l  @  l');[];v))\mdownarrow{}


By

---

Latex:
(GenConclAtAddrType  \mkleeneopen{}Top  List\mkleeneclose{}  [1]\mcdot{}  THEN  Auto)

---

Home Index