---

Step * of Lemma corec-subtype-corec

∀[F,G:Type ⟶ Type].  (corec(T.F[T]) ⊆r corec(T.G[T])) supposing (Monotone(T.G[T]) and (∀T:Type. (F[T] ⊆r G[T])))
BY
{ (Auto THEN SubsumeC ⌜G A⌝⋅ THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[F,G:Type  {}\mrightarrow{}  Type].
    (corec(T.F[T])  \msubseteq{}r  corec(T.G[T]))  supposing  (Monotone(T.G[T])  and  (\mforall{}T:Type.  (F[T]  \msubseteq{}r  G[T])))


By

---

Latex:
(Auto  THEN  SubsumeC  \mkleeneopen{}G  A\mkleeneclose{}\mcdot{}  THEN  Auto)

---

Home Index