---

Step * 1 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
{ (((RW assert_pushdownC (-1) THENA Auto) THEN HypSubst (-1) 0) THEN Easy) }

---

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.  \muparrow{}null(L)
\mvdash{}  L  \msubseteq{}  L1


By

---

Latex:
(((RW  assert\_pushdownC  (-1)  THENA  Auto)  THEN  HypSubst  (-1)  0)  THEN  Easy)

---

Home Index