---

Step * of Lemma corec_subtype

∀[F:Type ⟶ Type]. corec(T.F[T]) ⊆r F[corec(T.F[T])] supposing Continuous(T.F[T])
BY
{ (Auto
   THEN (With ⌜λn.primrec(n;Top;λ,T. F[T])⌝ (D 2)⋅ THEN Auto)
   THEN Reduce (-1)
   THEN Fold `corec` (-1)
   THEN Using [`B',⌜⋂n:ℕ. F[primrec(n;Top;λ,T. F[T])]⌝] (BLemma `subtype_rel_transitivity`)⋅
   THEN Try (Complete (Auto))) }

1
1. F : Type ⟶ Type
2. (⋂n:ℕ. F[primrec(n;Top;λ,T. F[T])]) ⊆r F[corec(T.F[T])]
⊢ corec(T.F[T]) ⊆r (⋂n:ℕ. F[primrec(n;Top;λ,T. F[T])])

---

Latex:

---

Latex:
\mforall{}[F:Type  {}\mrightarrow{}  Type].  corec(T.F[T])  \msubseteq{}r  F[corec(T.F[T])]  supposing  Continuous(T.F[T])


By

---

Latex:
(Auto
  THEN  (With  \mkleeneopen{}\mlambda{}n.primrec(n;Top;\mlambda{},T.  F[T])\mkleeneclose{}  (D  2)\mcdot{}  THEN  Auto)
  THEN  Reduce  (-1)
  THEN  Fold  `corec`  (-1)
  THEN  Using  [`B',\mkleeneopen{}\mcap{}n:\mBbbN{}.  F[primrec(n;Top;\mlambda{},T.  F[T])]\mkleeneclose{}]  (BLemma  `subtype\_rel\_transitivity`)\mcdot{}
  THEN  Try  (Complete  (Auto)))

---

Home Index