---

Step * 1 2 1 of Lemma last-cons


1. x : Top
2. u : Top
3. v : Top List
⊢ [u / v][||v||] ~ [u / v][(||v|| + 1) - 1]
BY
{ (EqCD THEN Auto THEN Auto') }

---

Latex:

---

Latex:

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


By

---

Latex:
(EqCD  THEN  Auto  THEN  Auto')

---

Home Index