---

Step * of Lemma interleaving_sublist

∀[T:Type]. ∀L,L1,L2:T List.  (interleaving(T;L1;L2;L) ⇒ L1 ⊆ L)
BY
{ ((((((Unfolds ``interleaving sublist`` 0 THEN Unfold `disjoint_sublists` 0) THEN Auto') THEN ExRepD)
     THEN InstConcl [f1]
     )
    THEN Auto'
    )
   THEN EasyHyp
   ) }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}L,L1,L2:T  List.    (interleaving(T;L1;L2;L)  {}\mRightarrow{}  L1  \msubseteq{}  L)


By

---

Latex:
((((((Unfolds  ``interleaving  sublist``  0  THEN  Unfold  `disjoint\_sublists`  0)  THEN  Auto')  THEN  ExRepD)
      THEN  InstConcl  [f1]
      )
    THEN  Auto'
    )
  THEN  EasyHyp
  )

---

Home Index