---

Step * of Lemma l-ordered-sublist

∀[A:Type]. ∀R:A ⟶ A ⟶ ℙ. ∀as,bs:A List.  (as ⊆ bs ⇒ l-ordered(A;x,y.R[x;y];bs) ⇒ l-ordered(A;x,y.R[x;y];as))
BY
{ (Auto THEN All(Unfold `l-ordered`) THEN RepeatFor 3 (ParallelLast) THEN FLemma `l_before_sublist` [-6] THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[A:Type]
    \mforall{}R:A  {}\mrightarrow{}  A  {}\mrightarrow{}  \mBbbP{}.  \mforall{}as,bs:A  List.
        (as  \msubseteq{}  bs  {}\mRightarrow{}  l-ordered(A;x,y.R[x;y];bs)  {}\mRightarrow{}  l-ordered(A;x,y.R[x;y];as))


By

---

Latex:
(Auto
  THEN  All(Unfold  `l-ordered`)
  THEN  RepeatFor  3  (ParallelLast)
  THEN  FLemma  `l\_before\_sublist`  [-6]
  THEN  Auto)

---

Home Index