---

Step * 2 of Lemma corec-ext1


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])
BY
{ (RWO "primrec-unroll" 0 THEN Auto THEN AutoSplit) }

---

Latex:

---

Latex:

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


By

---

Latex:
(RWO  "primrec-unroll"  0  THEN  Auto  THEN  AutoSplit)

---

Home Index