---

Step * of Lemma compat-iseg

∀[T:Type]. ∀L1,L2,L3:T List.  (L1 ≤ L2 ⇒ L2 || L3 ⇒ L1 || L3)
BY
{ (((Unfold `iseg` 0
     THEN Auto
     THEN ExRepD
     THEN (InstLemma `compat-append` [⌜T⌝; ⌜L1⌝; ⌜L3⌝; ⌜l⌝; ⌜[]⌝])⋅
     THEN Auto
     THEN RWO "append_nil_sq" 0)
    THENA Auto
    )
   THEN (RevHypSubst (-2) 0)
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}L1,L2,L3:T  List.    (L1  \mleq{}  L2  {}\mRightarrow{}  L2  ||  L3  {}\mRightarrow{}  L1  ||  L3)


By

---

Latex:
(((Unfold  `iseg`  0
      THEN  Auto
      THEN  ExRepD
      THEN  (InstLemma  `compat-append`  [\mkleeneopen{}T\mkleeneclose{};  \mkleeneopen{}L1\mkleeneclose{};  \mkleeneopen{}L3\mkleeneclose{};  \mkleeneopen{}l\mkleeneclose{};  \mkleeneopen{}[]\mkleeneclose{}])\mcdot{}
      THEN  Auto
      THEN  RWO  "append\_nil\_sq"  0)
    THENA  Auto
    )
  THEN  (RevHypSubst  (-2)  0)
  THEN  Auto)

---

Home Index