---

Step * 1 of Lemma last-cons


1. x : Top
2. u : Top
3. v : Top List
⊢ [x; [u / v]][((||v|| + 1) + 1) - 1] ~ [u / v][(||v|| + 1) - 1]
BY
{ Subst ⌜((||v|| + 1) + 1) - 1 ~ ||v|| + 1⌝ 0 ⋅ }

1
.....equality..... 
1. x : Top
2. u : Top
3. v : Top List
⊢ ((||v|| + 1) + 1) - 1 ~ ||v|| + 1

2
1. x : Top
2. u : Top
3. v : Top List
⊢ [x; [u / v]][||v|| + 1] ~ [u / v][(||v|| + 1) - 1]

---

Latex:

---

Latex:

1.  x  :  Top
2.  u  :  Top
3.  v  :  Top  List
\mvdash{}  [x;  [u  /  v]][((||v||  +  1)  +  1)  -  1]  \msim{}  [u  /  v][(||v||  +  1)  -  1]


By

---

Latex:
Subst  \mkleeneopen{}((||v||  +  1)  +  1)  -  1  \msim{}  ||v||  +  1\mkleeneclose{}  0  \mcdot{}

---

Home Index