---

Step * 1 of Lemma firstn_length

.....truecase..... 
1. u : Top
2. v : Top List
3. firstn(||v||;v) ~ v
4. 0 < ||v|| + 1
⊢ [u / firstn((||v|| + 1) - 1;v)] ~ [u / v]
BY
{ (EqCD THEN Try (Trivial)) }

1
1. u : Top
2. v : Top List
3. firstn(||v||;v) ~ v
4. 0 < ||v|| + 1
⊢ firstn((||v|| + 1) - 1;v) ~ v

---

Latex:

---

Latex:
.....truecase..... 
1.  u  :  Top
2.  v  :  Top  List
3.  firstn(||v||;v)  \msim{}  v
4.  0  <  ||v||  +  1
\mvdash{}  [u  /  firstn((||v||  +  1)  -  1;v)]  \msim{}  [u  /  v]


By

---

Latex:
(EqCD  THEN  Try  (Trivial))

---

Home Index