---

Step * of Lemma is-list-wf-co-list

∀[T:Type]. ∀[t:colist(T)].  (is-list(t) ∈ partial(𝔹))
BY
{ ((UnivCD THENA Auto)
   THEN RepUR ``is-list`` 0
   THEN (InstLemma `fixpoint-induction-bottom` [⌜𝔹⌝;⌜colist(T) ⟶ partial(𝔹)⌝;⌜λ2x.x t⌝]⋅
   THENM (BHyp (-1) THEN Fold `is-list-fun` 0 THEN Auto)
   )
   THEN Try (BLemma `bool-mono`)
   THEN (Try (Complete (Auto)) THEN FunExt THEN Strictness THEN Auto)) }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[t:colist(T)].    (is-list(t)  \mmember{}  partial(\mBbbB{}))


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  RepUR  ``is-list``  0
  THEN  (InstLemma  `fixpoint-induction-bottom`  [\mkleeneopen{}\mBbbB{}\mkleeneclose{};\mkleeneopen{}colist(T)  {}\mrightarrow{}  partial(\mBbbB{})\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}x.x  t\mkleeneclose{}]\mcdot{}
  THENM  (BHyp  (-1)  THEN  Fold  `is-list-fun`  0  THEN  Auto)
  )
  THEN  Try  (BLemma  `bool-mono`)
  THEN  (Try  (Complete  (Auto))  THEN  FunExt  THEN  Strictness  THEN  Auto))

---

Home Index