---

Step * of Lemma length-append

∀[as,bs:Top].  (||as @ bs|| ~ ||as|| + ||bs||)
BY
{ ListIndSq `as' }

1
1. bs : Base
2. as : Base
3. x : Base@i
4. y : Base@i
5. r1 : Base@i
6. r2 : Base@i
7. ||r1|| ≤ r2 + ||bs||@i
⊢ ||r1|| + 1 ≤ (r2 + 1) + ||bs||

2
1. bs : Base
2. as : Base
3. x : Base@i
4. y : Base@i
5. r1 : Base@i
6. r2 : Base@i
7. r1 + ||bs|| ≤ ||r2||@i
⊢ (r1 + 1) + ||bs|| ≤ ||r2|| + 1

3
.....antecedent..... 
1. bs : Base
2. as : Base
⊢ ||bs|| ~ 0 + ||bs||

---

Latex:

---

Latex:
\mforall{}[as,bs:Top].    (||as  @  bs||  \msim{}  ||as||  +  ||bs||)


By

---

Latex:
ListIndSq  `as'

---

Home Index