---

Step * of Lemma sublist_append_front

∀[T:Type]. ∀L,L1,L2:T List.  L ⊆ L1 @ L2 ⇒ L ⊆ L1 supposing ¬(last(L) ∈ L2) supposing ¬↑null(L)
BY
{ ((Auto THEN Decide ↑null(L)) THENA Auto) }

1
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

2
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

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}L,L1,L2:T  List.    L  \msubseteq{}  L1  @  L2  {}\mRightarrow{}  L  \msubseteq{}  L1  supposing  \mneg{}(last(L)  \mmember{}  L2)  supposing  \mneg{}\muparrow{}null(L)


By

---

Latex:
((Auto  THEN  Decide  \muparrow{}null(L))  THENA  Auto)

---

Home Index