---

Step * 2 of Lemma sublist_append_front


1. [T] : Type
2. L : T List
3. L1 : T List
4. L2 : T List
5. ¬(last(L) ∈ L2) supposing ¬↑null(L)
6. L ⊆ L1 @ L2
7. ¬↑null(L)
⊢ L ⊆ L1
BY
{ ThinTrivial }

1
1. [T] : Type
2. L : T List
3. L1 : T List
4. L2 : T List
5. L ⊆ L1 @ L2
6. ¬↑null(L)
7. ¬(last(L) ∈ L2)
⊢ L ⊆ L1

---

Latex:

---

Latex:

1.  [T]  :  Type
2.  L  :  T  List
3.  L1  :  T  List
4.  L2  :  T  List
5.  \mneg{}(last(L)  \mmember{}  L2)  supposing  \mneg{}\muparrow{}null(L)
6.  L  \msubseteq{}  L1  @  L2
7.  \mneg{}\muparrow{}null(L)
\mvdash{}  L  \msubseteq{}  L1


By

---

Latex:
ThinTrivial

---

Home Index