---

Step * of Lemma member-co-list-islist

∀[T:Type]. ∀[L:colist(T)].  L ∈ co-list-islist(T) supposing (is-list(L))↓
BY
{ (RepeatFor 2 (Intro)
   THEN (InstLemma `is-list-wf-co-list` [⌜T⌝;⌜L⌝]⋅ THENA Auto)
   THEN (Assert (is-list(L))↓ ∈ Type BY
               Auto)
   THEN (D 0 THENA Auto)
   THEN (At ⌜Type⌝ MemTypeCD⋅ THEN Try (Trivial))
   THEN InstLemma `is-list-wf-co-list` [⌜T⌝;⌜L1⌝]⋅
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[L:colist(T)].    L  \mmember{}  co-list-islist(T)  supposing  (is-list(L))\mdownarrow{}


By

---

Latex:
(RepeatFor  2  (Intro)
  THEN  (InstLemma  `is-list-wf-co-list`  [\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}L\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (Assert  (is-list(L))\mdownarrow{}  \mmember{}  Type  BY
                          Auto)
  THEN  (D  0  THENA  Auto)
  THEN  (At  \mkleeneopen{}Type\mkleeneclose{}  MemTypeCD\mcdot{}  THEN  Try  (Trivial))
  THEN  InstLemma  `is-list-wf-co-list`  [\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}L1\mkleeneclose{}]\mcdot{}
  THEN  Auto)

---

Home Index