---

Step * 3 of Lemma length-rev-append


1. bs : Base
2. as : Base
3. x : Base@i
⊢ ||x|| ~ 0 + ||x||
BY
{ (ListIndSq `x' THEN ∀h:hyp. ImpossibleException h  THEN RWO  "add-associates<" 0 THEN Auto) }

---

Latex:

---

Latex:

1.  bs  :  Base
2.  as  :  Base
3.  x  :  Base@i
\mvdash{}  ||x||  \msim{}  0  +  ||x||


By

---

Latex:
(ListIndSq  `x'  THEN  \mforall{}h:hyp.  ImpossibleException  h    THEN  RWO    "add-associates<"  0  THEN  Auto)

---

Home Index