---

Step * of Lemma l-ordered-remove-combine

∀T:Type. ∀R:T ⟶ T ⟶ ℙ. ∀cmp:T ⟶ ℤ. ∀L:T List.
  (l-ordered(T;x,y.R[x;y];L) ⇒ l-ordered(T;x,y.R[x;y];remove-combine(cmp;L)))
BY
{ xxx(InductionOnList
      THEN RW ListC 0
      THEN Auto
      THEN Repeat (AutoSplit)
      THEN RW ListC 0
      THEN Auto
      THEN FLemma `remove-combine-implies-member` [-1]
      THEN Auto)xxx }

---

Latex:

---

Latex:
\mforall{}T:Type.  \mforall{}R:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}.  \mforall{}cmp:T  {}\mrightarrow{}  \mBbbZ{}.  \mforall{}L:T  List.
    (l-ordered(T;x,y.R[x;y];L)  {}\mRightarrow{}  l-ordered(T;x,y.R[x;y];remove-combine(cmp;L)))


By

---

Latex:
xxx(InductionOnList
        THEN  RW  ListC  0
        THEN  Auto
        THEN  Repeat  (AutoSplit)
        THEN  RW  ListC  0
        THEN  Auto
        THEN  FLemma  `remove-combine-implies-member`  [-1]
        THEN  Auto)xxx

---

Home Index