---

Step * of Lemma is-list-fun_wf

∀[T:Type]. (is-list-fun() ∈ (colist(T) ⟶ partial(𝔹)) ⟶ colist(T) ⟶ partial(𝔹))
BY
{ (ProveWfLemma
   THEN (InstLemma `co-list-has-value` [⌜T⌝;⌜t⌝]⋅ THENA Auto)
   THEN GenConclAtAddrType ⌜Unit ⋃ (T × colist(T))⌝ [2;1]⋅
   THEN Try (Complete (Auto))
   THEN Thin (-1)
   THEN (ListUnionDAux `u' `v' (-1) THENA Auto)
   THEN RepUR ``cons nil`` 0
   THEN Auto)⋅ }

---

Latex:

---

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


By

---

Latex:
(ProveWfLemma
  THEN  (InstLemma  `co-list-has-value`  [\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}t\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  GenConclAtAddrType  \mkleeneopen{}Unit  \mcup{}  (T  \mtimes{}  colist(T))\mkleeneclose{}  [2;1]\mcdot{}
  THEN  Try  (Complete  (Auto))
  THEN  Thin  (-1)
  THEN  (ListUnionDAux  `u'  `v'  (-1)  THENA  Auto)
  THEN  RepUR  ``cons  nil``  0
  THEN  Auto)\mcdot{}

---

Home Index