---

Step * 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'
⊢ last(L') = last(L) ∈ T
BY
{ (FLemma `last-not-before` [-1] THEN Auto) }

1
.....antecedent..... 
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'
⊢ no_repeats(T;L')

---

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'
\mvdash{}  last(L')  =  last(L)


By

---

Latex:
(FLemma  `last-not-before`  [-1]  THEN  Auto)

---

Home Index