---

Step * 1 2 of Lemma last-cons


1. x : Top
2. u : Top
3. v : Top List
⊢ [x; [u / v]][||v|| + 1] ~ [u / v][(||v|| + 1) - 1]
BY
{ (RWO "select_cons_tl_sq" 0 THENA Auto') }

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

---

Latex:

---

Latex:

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


By

---

Latex:
(RWO  "select\_cons\_tl\_sq"  0  THENA  Auto')

---

Home Index