---

Step * of Lemma bigrel_wf

∀[T:𝕌']. ∀[F:(T ⟶ T ⟶ ℙ) ⟶ T ⟶ T ⟶ ℙ].  (νR.F[R] ∈ T ⟶ T ⟶ ℙ)
BY
{ RepeatFor 2 (ProveWfLemma)⋅ }

---

Latex:

---

Latex:
\mforall{}[T:\mBbbU{}'].  \mforall{}[F:(T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{})  {}\mrightarrow{}  T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}].    (\mnu{}R.F[R]  \mmember{}  T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{})


By

---

Latex:
RepeatFor  2  (ProveWfLemma)\mcdot{}

---

Home Index