---

Step * of Lemma last_append

∀[A,B:Top List].  last(A @ B) ~ last(B) supposing ¬↑null(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 ¬↑null(B)
4. B : Top List
5. ¬↑null(B)
⊢ last([u / (v @ B)]) ~ last(B)

---

Latex:

---

Latex:
\mforall{}[A,B:Top  List].    last(A  @  B)  \msim{}  last(B)  supposing  \mneg{}\muparrow{}null(B)


By

---

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

---

Home Index