---

Step * 1 of Lemma corec-greatest

.....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]))
BY
{ (InductionOnNat THEN (RWO "primrec-unroll" 0 THENA Auto) THEN Reduce 0 THEN Try (SplitOnConclITE) THEN Auto) }

---

Latex:

---

Latex:
.....assertion..... 
1.  [F]  :  Type  {}\mrightarrow{}  Type
2.  [\%]  :  Monotone(T.F[T])
3.  [X]  :  Type
4.  [\%1]  :  X  \mequiv{}  F[X]
\mvdash{}  \mforall{}n:\mBbbN{}.  (X  \msubseteq{}r  primrec(n;Top;\mlambda{},T.  F[T]))


By

---

Latex:
(InductionOnNat
  THEN  (RWO  "primrec-unroll"  0  THENA  Auto)
  THEN  Reduce  0
  THEN  Try  (SplitOnConclITE)
  THEN  Auto)

---

Home Index