---

Step * of Lemma is-list_wf

∀[T:Type]. ∀[t:colist(T)].  (is-list(t) ∈ partial(𝔹))
BY
{ ((Auto
    THEN Unfold `colist` -1
    THEN Unfold `is-list` 0
    THEN InstLemma `fix_wf_corec-partial1` [⌜𝔹⌝;⌜λ2L.Unit ⋃ (T × L)⌝;⌜λis-list,t. eval u = t in
                                                                                  if u is a pair then is-list (snd(u))
                                                                                  otherwise if u = Ax then tt
                                                                                            otherwise ⊥⌝]⋅
    THEN Auto)
   THEN D_b_union (-1)
   THEN D -1
   THEN Reduce 0
   THEN Auto) }

---

Latex:

---

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


By

---

Latex:
((Auto
    THEN  Unfold  `colist`  -1
    THEN  Unfold  `is-list`  0
    THEN  InstLemma  `fix\_wf\_corec-partial1`  [\mkleeneopen{}\mBbbB{}\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}L.Unit  \mcup{}  (T  \mtimes{}  L)\mkleeneclose{};
    \mkleeneopen{}\mlambda{}is-list,t.  eval  u  =  t  in
                              if  u  is  a  pair  then  is-list  (snd(u))  otherwise  if  u  =  Ax  then  tt  otherwise  \mbot{}\mkleeneclose{}]\mcdot{}
    THEN  Auto)
  THEN  D\_b\_union  (-1)
  THEN  D  -1
  THEN  Reduce  0
  THEN  Auto)

---

Home Index