---

Step * of Lemma subtype_urec

∀[F:Type ⟶ Type]. (F urec(F)) ⊆r urec(F) supposing continuous'-monotone{i:l}(T.F T)
BY
{ ((Auto THEN D -1)
   THEN (With ⌜λn.(F^n Void)⌝ (D 3)⋅ THEN Try (BLemma `monotone-incr-chain`) THEN Auto)
   THEN Reduce (-1)
   THEN Fold `urec` (-1)
   THEN Using [`B',⌜⋃n:ℕ.(F (F^n Void))⌝] (BLemma `subtype_rel_transitivity`)⋅
   THEN Try (Complete (Auto)))⋅ }

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

---

Latex:

---

Latex:
\mforall{}[F:Type  {}\mrightarrow{}  Type].  (F  urec(F))  \msubseteq{}r  urec(F)  supposing  continuous'-monotone\{i:l\}(T.F  T)


By

---

Latex:
((Auto  THEN  D  -1)
  THEN  (With  \mkleeneopen{}\mlambda{}n.(F\^{}n  Void)\mkleeneclose{}  (D  3)\mcdot{}  THEN  Try  (BLemma  `monotone-incr-chain`)  THEN  Auto)
  THEN  Reduce  (-1)
  THEN  Fold  `urec`  (-1)
  THEN  Using  [`B',\mkleeneopen{}\mcup{}n:\mBbbN{}.(F  (F\^{}n  Void))\mkleeneclose{}]  (BLemma  `subtype\_rel\_transitivity`)\mcdot{}
  THEN  Try  (Complete  (Auto)))\mcdot{}

---

Home Index