---

Step * of Lemma corec-ext1

∀[F:Type ⟶ Type]. corec(T.F[T]) ≡ F[corec(T.F[T])] supposing Continuous+(T.F[T])
BY
{ (Auto
   THEN Unfold `corec` 0
   THEN With ⌜λn.primrec(n;Top;λj,T. F[T])⌝ (D (-1))⋅
   THEN Reduce (-1)
   THEN Auto
   THEN Assert ⌜⋂n:ℕ. primrec(n;Top;λj,T. F[T]) ≡ ⋂n:ℕ. F[primrec(n;Top;λj,T. F[T])]⌝⋅
   THEN Try ((RelRST THEN Auto))
   THEN Thin (-1)
   THEN RepeatFor 2 ((D 0 THENA Auto))
   THEN Auto) }

1
1. F : Type ⟶ Type
2. x : ⋂n:ℕ. primrec(n;Top;λj,T. F[T])
3. n : ℕ
⊢ x ∈ F[primrec(n;Top;λj,T. F[T])]

2
1. F : Type ⟶ Type
2. x : ⋂n:ℕ. F[primrec(n;Top;λj,T. F[T])]
3. n : ℕ
⊢ x ∈ primrec(n;Top;λj,T. F[T])

---

Latex:

---

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


By

---

Latex:
(Auto
  THEN  Unfold  `corec`  0
  THEN  With  \mkleeneopen{}\mlambda{}n.primrec(n;Top;\mlambda{}j,T.  F[T])\mkleeneclose{}  (D  (-1))\mcdot{}
  THEN  Reduce  (-1)
  THEN  Auto
  THEN  Assert  \mkleeneopen{}\mcap{}n:\mBbbN{}.  primrec(n;Top;\mlambda{}j,T.  F[T])  \mequiv{}  \mcap{}n:\mBbbN{}.  F[primrec(n;Top;\mlambda{}j,T.  F[T])]\mkleeneclose{}\mcdot{}
  THEN  Try  ((RelRST  THEN  Auto))
  THEN  Thin  (-1)
  THEN  RepeatFor  2  ((D  0  THENA  Auto))
  THEN  Auto)

---

Home Index