---

Step * of Lemma iseg-sorted-by

∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].  ∀sa,sb:T List.  (sa ≤ sb ⇒ sorted-by(R;sb) ⇒ sorted-by(R;sa))
BY
{ (InstLemma `sublist-sorted-by` [] THEN RepeatFor 5 ((ParallelLast' THENA Auto))) }

1
.....antecedent..... 
1. [T] : Type
2. [R] : T ⟶ T ⟶ ℙ
3. sa : T List@i
4. sb : T List@i
5. sa ≤ sb@i
⊢ sa ⊆ sb

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[R:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}].    \mforall{}sa,sb:T  List.    (sa  \mleq{}  sb  {}\mRightarrow{}  sorted-by(R;sb)  {}\mRightarrow{}  sorted-by(R;sa))


By

---

Latex:
(InstLemma  `sublist-sorted-by`  []  THEN  RepeatFor  5  ((ParallelLast'  THENA  Auto)))

---

Home Index