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