---

Step * of Lemma sorted-by-single

∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].  ∀x:T. sorted-by(R;[x])
BY
{ (Auto THEN D 0 THEN All Reduce THEN Auto') }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[R:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}].    \mforall{}x:T.  sorted-by(R;[x])


By

---

Latex:
(Auto  THEN  D  0  THEN  All  Reduce  THEN  Auto')

---

Home Index