---

Step * 1 of Lemma colist-fix-ap-partial


1. A : Type
2. value-type(A)
3. mono(A)
4. T : Type
5. f : ⋂L:Type. ((L ⟶ partial(A)) ⟶ (Unit ⋃ (T × L)) ⟶ partial(A))
6. L : colist(T)
7. fix(f) ∈ colist(T) ⟶ partial(A)
⊢ fix(f) L ∈ partial(A)
BY
{ Auto }

---

Latex:

---

Latex:

1.  A  :  Type
2.  value-type(A)
3.  mono(A)
4.  T  :  Type
5.  f  :  \mcap{}L:Type.  ((L  {}\mrightarrow{}  partial(A))  {}\mrightarrow{}  (Unit  \mcup{}  (T  \mtimes{}  L))  {}\mrightarrow{}  partial(A))
6.  L  :  colist(T)
7.  fix(f)  \mmember{}  colist(T)  {}\mrightarrow{}  partial(A)
\mvdash{}  fix(f)  L  \mmember{}  partial(A)


By

---

Latex:
Auto

---

Home Index