---

Step * 1 of Lemma colist-unfold_wf


1. A : Type
2. B : Type
3. P : B ⟶ (Unit + (A × B))
4. x : B
⊢ fix((λcolist-unfold,x. case P x of inl(u) => [] | inr(v) => let a,b = v in [a / (colist-unfold b)])) x ∈ corec(L.Unit \000C⋃ (A × L))
BY
{ xxx(BLemma `fix_wf_corec_parameter` THEN RepUR ``nil cons`` 0 THEN Auto)xxx }

---

Latex:

---

Latex:

1.  A  :  Type
2.  B  :  Type
3.  P  :  B  {}\mrightarrow{}  (Unit  +  (A  \mtimes{}  B))
4.  x  :  B
\mvdash{}  fix((\mlambda{}colist-unfold,x.  case  P  x  of  inl(u)  =>  []  |  inr(v)  =>  let  a,b  =  v  in  [a  /  (colist-unfold  b)]\000C))  x
    \mmember{}  corec(L.Unit  \mcup{}  (A  \mtimes{}  L))


By

---

Latex:
xxx(BLemma  `fix\_wf\_corec\_parameter`  THEN  RepUR  ``nil  cons``  0  THEN  Auto)xxx

---

Home Index