---

Step * of Lemma rel-monotone_wf

∀[T:Type]. ∀[F:(T ⟶ T ⟶ ℙ) ⟶ T ⟶ T ⟶ ℙ].  (rel-monotone{i:l}(T;R.F[R]) ∈ ℙ')
BY
{ ProveWfLemma }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[F:(T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{})  {}\mrightarrow{}  T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}].    (rel-monotone\{i:l\}(T;R.F[R])  \mmember{}  \mBbbP{}')


By

---

Latex:
ProveWfLemma

---

Home Index