---

Step * 1 of Lemma urec_subtype


1. F : Type ⟶ Type
2. Monotone(T.F[T])
⊢ urec(F) ⊆r ⋃n:ℕ.(F (F^n Void))
BY
{ Thin (-1) }

1
1. F : Type ⟶ Type
⊢ urec(F) ⊆r ⋃n:ℕ.(F (F^n Void))

---

Latex:

---

Latex:

1.  F  :  Type  {}\mrightarrow{}  Type
2.  Monotone(T.F[T])
\mvdash{}  urec(F)  \msubseteq{}r  \mcup{}n:\mBbbN{}.(F  (F\^{}n  Void))


By

---

Latex:
Thin  (-1)

---

Home Index