---

Step * 2 1 of Lemma sublist-same-last


1. T : Type
2. L : T List
3. L' : T List
4. ¬↑null(L)
5. no_repeats(T;L)
6. ¬↑null(L')
7. L' ⊆ L
8. (last(L) ∈ L')
9. last(L) before last(L') ∈ L'
10. ∀x,y:T.  (x before y ∈ L' ⇒ x before y ∈ L)
11. last(L) before last(L') ∈ L
⊢ last(L') = last(L) ∈ T
BY
{ (FLemma `last-not-before` [-1] THEN Auto)⋅ }

---

Latex:

---

Latex:

1.  T  :  Type
2.  L  :  T  List
3.  L'  :  T  List
4.  \mneg{}\muparrow{}null(L)
5.  no\_repeats(T;L)
6.  \mneg{}\muparrow{}null(L')
7.  L'  \msubseteq{}  L
8.  (last(L)  \mmember{}  L')
9.  last(L)  before  last(L')  \mmember{}  L'
10.  \mforall{}x,y:T.    (x  before  y  \mmember{}  L'  {}\mRightarrow{}  x  before  y  \mmember{}  L)
11.  last(L)  before  last(L')  \mmember{}  L
\mvdash{}  last(L')  =  last(L)


By

---

Latex:
(FLemma  `last-not-before`  [-1]  THEN  Auto)\mcdot{}

---

Home Index