---

Step * 1 1 of Lemma sublist_interleaved


1. [T] : Type
2. L1 : T List
3. L1 ⊆ []
⊢ interleaving(T;L1;[];[])
BY
{ ((((RWO "sublist_nil" (-1) THENA Auto{1,4}-1) THEN HypSubst (-1) 0) THENA Auto) THEN Easy) }

---

Latex:

---

Latex:

1.  [T]  :  Type
2.  L1  :  T  List
3.  L1  \msubseteq{}  []
\mvdash{}  interleaving(T;L1;[];[])


By

---

Latex:
((((RWO  "sublist\_nil"  (-1)  THENA  Auto\{1,4\}-1)  THEN  HypSubst  (-1)  0)  THENA  Auto)  THEN  Easy)

---

Home Index