---

Step * 1 of Lemma sorted-filter


1. T : Type
2. T ⊆r ℤ
3. P : T ⟶ 𝔹
⊢ sorted([]) ⇒ sorted([])
BY
{ At ⌜Type⌝ (Using [`T',⌜T⌝]  Auto)⋅ }

---

Latex:

---

Latex:

1.  T  :  Type
2.  T  \msubseteq{}r  \mBbbZ{}
3.  P  :  T  {}\mrightarrow{}  \mBbbB{}
\mvdash{}  sorted([])  {}\mRightarrow{}  sorted([])


By

---

Latex:
At  \mkleeneopen{}Type\mkleeneclose{}  (Using  [`T',\mkleeneopen{}T\mkleeneclose{}]    Auto)\mcdot{}

---

Home Index