---

Step * of Lemma sublist-same-last

∀[T:Type]. ∀[L,L':T List].
  (last(L') = last(L) ∈ T) supposing ((last(L) ∈ L') and L' ⊆ L and (¬↑null(L')) and no_repeats(T;L) and (¬↑null(L)))
BY
{ (Auto THEN (InstLemma `l_tricotomy` [⌜T⌝;⌜last(L')⌝;⌜last(L)⌝;⌜L'⌝]⋅ THEN Auto) THEN SplitOrHyps 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'
⊢ last(L') = last(L) ∈ T

2
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

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[L,L':T  List].
    (last(L')  =  last(L))  supposing 
          ((last(L)  \mmember{}  L')  and 
          L'  \msubseteq{}  L  and 
          (\mneg{}\muparrow{}null(L'))  and 
          no\_repeats(T;L)  and 
          (\mneg{}\muparrow{}null(L)))


By

---

Latex:
(Auto
  THEN  (InstLemma  `l\_tricotomy`  [\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}last(L')\mkleeneclose{};\mkleeneopen{}last(L)\mkleeneclose{};\mkleeneopen{}L'\mkleeneclose{}]\mcdot{}  THEN  Auto)
  THEN  SplitOrHyps
  THEN  Auto)

---

Home Index