---

Step * of Lemma last_append2

∀[A,B:Top List].  last(A @ B) ~ last(B) supposing 0 < ||B||
BY
{ (((InductionOnList THEN Reduce 0 THEN UnivCD) THENA Auto) THEN Try (Trivial)) }

1
1. u : Top
2. v : Top List
3. ∀[B:Top List]. last(v @ B) ~ last(B) supposing 0 < ||B||
4. B : Top List
5. 0 < ||B||
⊢ last([u / (v @ B)]) ~ last(B)

---

Latex:

---

Latex:
\mforall{}[A,B:Top  List].    last(A  @  B)  \msim{}  last(B)  supposing  0  <  ||B||


By

---

Latex:
(((InductionOnList  THEN  Reduce  0  THEN  UnivCD)  THENA  Auto)  THEN  Try  (Trivial))

---

Home Index