---

Step * of Lemma length-rev-append

∀[as,bs:Top].  (||rev(as) + bs|| ~ ||as|| + ||bs||)
BY
{ (ListAccumListIndSq `as' THEN (UnivCD THENA Auto)) }

1
1. bs : Base
2. as : Base
3. z : Base@i
⊢ strict1(λx.(x + ||z||))

2
1. bs : Base
2. as : Base
3. a : Base@i
4. b : Base@i
5. c : Base@i
⊢ c + ||b|| + 1 ~ (c + 1) + ||b||

3
1. bs : Base
2. as : Base
3. x : Base@i
⊢ ||x|| ~ 0 + ||x||

---

Latex:

---

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


By

---

Latex:
(ListAccumListIndSq  `as'  THEN  (UnivCD  THENA  Auto))

---

Home Index