---

Step * of Lemma iseg_is_sublist

∀[T:Type]. ∀L_1,L_2:T List.  (L_1 ≤ L_2 ⇒ L_1 ⊆ L_2)
BY
{ xxx(((((Unfold `sublist` 0 THEN Auto THEN InstLemma `iseg_length` [T;L_1;L_2]⋅) THENA Auto)
        THEN InstLemma `iseg_select` [T;L_1;L_2]⋅
        )
       THENA Auto
       )
      THEN InstConcl [λi.i]⋅
      THEN Reduce 0
      THEN Auto'
      THEN Try ((BackThruLemma `id_increasing` THEN Auto')))xxx }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}L$_{1}$,L$_{2}$:T  List.    (L$_{1}\000C$  \mleq{}  L$_{2}$  {}\mRightarrow{}  L$_{1}$  \msubseteq{}  L$_{2}$)


By

---

Latex:
xxx(((((Unfold  `sublist`  0  THEN  Auto  THEN  InstLemma  `iseg\_length`  [T;L$_{1}$;L\mbackslash{}f\000Cf24_{2}$]\mcdot{})  THENA  Auto)
            THEN  InstLemma  `iseg\_select`  [T;L$_{1}$;L$_{2}$]\mcdot{}
            )
          THENA  Auto
          )
        THEN  InstConcl  [\mlambda{}i.i]\mcdot{}
        THEN  Reduce  0
        THEN  Auto'
        THEN  Try  ((BackThruLemma  `id\_increasing`  THEN  Auto')))xxx

---

Home Index