---

Step * of Lemma sublist_append1

∀[T:Type]. ∀L1,L2:T List.  L1 ⊆ L1 @ L2
BY
{ (Auto THEN With ⌜λx.x⌝ (D 0)⋅ THEN Reduce 0 THEN Auto' THEN Try ((D 0 THEN Reduce 0 THEN Auto')⋅)) }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}L1,L2:T  List.    L1  \msubseteq{}  L1  @  L2


By

---

Latex:
(Auto  THEN  With  \mkleeneopen{}\mlambda{}x.x\mkleeneclose{}  (D  0)\mcdot{}  THEN  Reduce  0  THEN  Auto'  THEN  Try  ((D  0  THEN  Reduce  0  THEN  Auto')\mcdot{}))

---

Home Index