---

Step * of Lemma corec-greatest

∀[F:Type ⟶ Type]. ∀[X:Type]. X ⊆r corec(T.F[T]) supposing X ≡ F[X] supposing Monotone(T.F[T])
BY
{ (Intros THEN Unfold `corec` 0 THEN Assert ⌜∀n:ℕ. (X ⊆r primrec(n;Top;λ,T. F[T]))⌝⋅) }

1
.....assertion..... 
1. [F] : Type ⟶ Type
2. [%] : Monotone(T.F[T])
3. [X] : Type
4. [%1] : X ≡ F[X]
⊢ ∀n:ℕ. (X ⊆r primrec(n;Top;λ,T. F[T]))

2
1. [F] : Type ⟶ Type
2. [%] : Monotone(T.F[T])
3. [X] : Type
4. [%1] : X ≡ F[X]
5. ∀n:ℕ. (X ⊆r primrec(n;Top;λ,T. F[T]))
⊢ X ⊆r (⋂n:ℕ. primrec(n;Top;λ,T. F[T]))

---

Latex:

---

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


By

---

Latex:
(Intros  THEN  Unfold  `corec`  0  THEN  Assert  \mkleeneopen{}\mforall{}n:\mBbbN{}.  (X  \msubseteq{}r  primrec(n;Top;\mlambda{},T.  F[T]))\mkleeneclose{}\mcdot{})

---

Home Index