---

Step * 1 1 of Lemma sublist-same-last

.....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')
BY
{ (FLemma `no_repeats-sublist` [5;7] THEN Auto) }

---

Latex:

---

Latex:
.....antecedent..... 
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{}  no\_repeats(T;L')


By

---

Latex:
(FLemma  `no\_repeats-sublist`  [5;7]  THEN  Auto)

---

Home Index