---

Step * 2 1 of Lemma urec_subtype


1. F : Type ⟶ Type
2. Monotone(T.F[T])
3. union-continuous{i:l}(T.F[T])
⊢ ⋃n:ℕ.(F (F^n Void)) ⊆r (F urec(F))
BY
{ (All (Unfolds ``union-continuous``)
   THEN (InstHyp [⌜ℕ⌝;⌜λn.(F^n Void)⌝] (-1)⋅ THENA Auto)
   THEN Reduce (-1)
   THEN Fold `urec` (-1)
   THEN Auto)⋅ }

---

Latex:

---

Latex:

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


By

---

Latex:
(All  (Unfolds  ``union-continuous``)
  THEN  (InstHyp  [\mkleeneopen{}\mBbbN{}\mkleeneclose{};\mkleeneopen{}\mlambda{}n.(F\^{}n  Void)\mkleeneclose{}]  (-1)\mcdot{}  THENA  Auto)
  THEN  Reduce  (-1)
  THEN  Fold  `urec`  (-1)
  THEN  Auto)\mcdot{}

---

Home Index