---

Step * 2 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 `l_before_sublist` [-3]⋅ THENA Auto) THEN FHyp (-1) [-2] THEN Auto) }

1
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

---

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  `l\_before\_sublist`  [-3]\mcdot{}  THENA  Auto)  THEN  FHyp  (-1)  [-2]  THEN  Auto)

---

Home Index