---

Step * of Lemma colist-fix-ap-partial

∀[A:Type]
  (∀[T:Type]. ∀[f:⋂L:Type. ((L ⟶ partial(A)) ⟶ (Unit ⋃ (T × L)) ⟶ partial(A))]. ∀[L:colist(T)].
     (fix(f) L ∈ partial(A))) supposing 
     (mono(A) and 
     value-type(A))
BY
{ (Intros THEN Unhide THEN (InstLemma `colist-fix-partial` [⌜A⌝;⌜T⌝;⌜f⌝]⋅ THENA Auto)) }

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

---

Latex:

---

Latex:
\mforall{}[A:Type]
    (\mforall{}[T:Type].  \mforall{}[f:\mcap{}L:Type.  ((L  {}\mrightarrow{}  partial(A))  {}\mrightarrow{}  (Unit  \mcup{}  (T  \mtimes{}  L))  {}\mrightarrow{}  partial(A))].  \mforall{}[L:colist(T)].
          (fix(f)  L  \mmember{}  partial(A)))  supposing 
          (mono(A)  and 
          value-type(A))


By

---

Latex:
(Intros  THEN  Unhide  THEN  (InstLemma  `colist-fix-partial`  [\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}f\mkleeneclose{}]\mcdot{}  THENA  Auto))

---

Home Index