---

Step * 2 2 1 1 1 2 of Lemma last-concat-non-null


1. T : Type
2. u : T List
3. u1 : T List
4. v : T List List
5. ¬False
6. ¬↑null(last([u1 / v]))
7. ¬↑null(concat([u1 / v]))
8. last(concat([u1 / v])) = last(last([u1 / v])) ∈ T
9. ¬↑null(u @ concat([u1 / v]))
⊢ last(u @ concat([u1 / v])) = last(last([u; [u1 / v]])) ∈ T
BY
{ (NthHypEq (-2) THEN EqCD THEN Auto) }

---

Latex:

---

Latex:

1.  T  :  Type
2.  u  :  T  List
3.  u1  :  T  List
4.  v  :  T  List  List
5.  \mneg{}False
6.  \mneg{}\muparrow{}null(last([u1  /  v]))
7.  \mneg{}\muparrow{}null(concat([u1  /  v]))
8.  last(concat([u1  /  v]))  =  last(last([u1  /  v]))
9.  \mneg{}\muparrow{}null(u  @  concat([u1  /  v]))
\mvdash{}  last(u  @  concat([u1  /  v]))  =  last(last([u;  [u1  /  v]]))


By

---

Latex:
(NthHypEq  (-2)  THEN  EqCD  THEN  Auto)

---

Home Index