---

Step * of Lemma list-at_wf

∀[T:Type]. ∀[ns:colist(ℕ)]. ∀[L:colist(T)].  (L@ns ∈ colist(T))
BY
{ (Auto
   THEN Unfold `colist` 0
   THEN Unfold `corec` 0
   THEN (MemTypeCD THENW Auto)
   THEN RepeatFor 2 (MoveToConcl (-2))
   THEN NatInd (-1)
   THEN Intros) }

1
1. T : Type
2. n : ℤ
3. ns : colist(ℕ)
4. L : colist(T)
⊢ L@ns ∈ primrec(0;Top;λ,L. (Unit ⋃ (T × L)))

2
1. T : Type
2. n : ℤ
3. 0 < n
4. ∀ns:colist(ℕ). ∀L:colist(T).  (L@ns ∈ primrec(n - 1;Top;λ,L. (Unit ⋃ (T × L))))
5. ns : colist(ℕ)
6. L : colist(T)
⊢ L@ns ∈ primrec(n;Top;λ,L. (Unit ⋃ (T × L)))

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[ns:colist(\mBbbN{})].  \mforall{}[L:colist(T)].    (L@ns  \mmember{}  colist(T))


By

---

Latex:
(Auto
  THEN  Unfold  `colist`  0
  THEN  Unfold  `corec`  0
  THEN  (MemTypeCD  THENW  Auto)
  THEN  RepeatFor  2  (MoveToConcl  (-2))
  THEN  NatInd  (-1)
  THEN  Intros)

---

Home Index