---

Step * of Lemma colist-unfold_wf

∀[A,B:Type]. ∀[P:B ⟶ (Unit + (A × B))]. ∀[x:B].  (colist-unfold(P;x) ∈ colist(A))
BY
{ (ProveWfLemma THEN Unfold `colist` 0) }

1
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))

---

Latex:

---

Latex:
\mforall{}[A,B:Type].  \mforall{}[P:B  {}\mrightarrow{}  (Unit  +  (A  \mtimes{}  B))].  \mforall{}[x:B].    (colist-unfold(P;x)  \mmember{}  colist(A))


By

---

Latex:
(ProveWfLemma  THEN  Unfold  `colist`  0)

---

Home Index