---

Step * of Lemma rel-continuous_wf

∀[T:Type]. ∀[F:(T ⟶ T ⟶ ℙ) ⟶ T ⟶ T ⟶ ℙ].  (rel-continuous{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-continuous\{i:l\}(T;R.F[R])  \mmember{}  \mBbbP{}')


By

---

Latex:
ProveWfLemma\mcdot{}

---

Home Index