---

Step * 1 of Lemma corec-ext1


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])]
BY
{ (SubsumeC ⌜primrec(n + 1;Top;λj,T. F[T])⌝⋅
   THEN (Auto THEN Unfold `so_apply` 0)
   THEN RW (AddrC [1] (LemmaC `primrec-unroll`)) 0
   THEN Reduce 0
   THEN Auto
   THEN OldAutoSplit) }

---

Latex:

---

Latex:

1.  F  :  Type  {}\mrightarrow{}  Type
2.  x  :  \mcap{}n:\mBbbN{}.  primrec(n;Top;\mlambda{}j,T.  F[T])
3.  n  :  \mBbbN{}
\mvdash{}  x  \mmember{}  F[primrec(n;Top;\mlambda{}j,T.  F[T])]


By

---

Latex:
(SubsumeC  \mkleeneopen{}primrec(n  +  1;Top;\mlambda{}j,T.  F[T])\mkleeneclose{}\mcdot{}
  THEN  (Auto  THEN  Unfold  `so\_apply`  0)
  THEN  RW  (AddrC  [1]  (LemmaC  `primrec-unroll`))  0
  THEN  Reduce  0
  THEN  Auto
  THEN  OldAutoSplit)

---

Home Index