---

Step * of Lemma conil_wf

∀[A:Type]. (conil() ∈ co-list-islist(A))
BY
{ (Auto
   THEN Unfolds ``conil co-list-islist`` 0
   THEN InstLemma `has-value-is-list-of-co-list` []
   THEN MemTypeCD
   THEN Auto) }

1
1. A : Type
2. ∀[T:Type]. ∀[t:colist(T)].  ((is-list(t))↓ ∈ ℙ)
⊢ Ax ∈ colist(A)

2
.....set predicate..... 
1. A : Type
2. ∀[T:Type]. ∀[t:colist(T)].  ((is-list(t))↓ ∈ ℙ)
⊢ (is-list(Ax))↓

---

Latex:

---

Latex:
\mforall{}[A:Type].  (conil()  \mmember{}  co-list-islist(A))


By

---

Latex:
(Auto
  THEN  Unfolds  ``conil  co-list-islist``  0
  THEN  InstLemma  `has-value-is-list-of-co-list`  []
  THEN  MemTypeCD
  THEN  Auto)

---

Home Index