---

Step * 1 of Lemma conil_wf


1. A : Type
2. ∀[T:Type]. ∀[t:colist(T)].  ((is-list(t))↓ ∈ ℙ)
⊢ Ax ∈ colist(A)
BY
{ (Fold `it` 0 THEN Auto)⋅ }

---

Latex:

---

Latex:

1.  A  :  Type
2.  \mforall{}[T:Type].  \mforall{}[t:colist(T)].    ((is-list(t))\mdownarrow{}  \mmember{}  \mBbbP{})
\mvdash{}  Ax  \mmember{}  colist(A)


By

---

Latex:
(Fold  `it`  0  THEN  Auto)\mcdot{}

---

Home Index