---

Step * 1 of Lemma sublist_interleaved


1. [T] : Type
⊢ ∀L1:T List. (L1 ⊆ [] ⇒ (∃L2:T List. interleaving(T;L1;L2;[])))
BY
{ ((Auto THEN InstConcl [[]]) THEN Auto) }

1
1. [T] : Type
2. L1 : T List
3. L1 ⊆ []
⊢ interleaving(T;L1;[];[])

---

Latex:

---

Latex:

1.  [T]  :  Type
\mvdash{}  \mforall{}L1:T  List.  (L1  \msubseteq{}  []  {}\mRightarrow{}  (\mexists{}L2:T  List.  interleaving(T;L1;L2;[])))


By

---

Latex:
((Auto  THEN  InstConcl  [[]])  THEN  Auto)

---

Home Index