---

Step * 1 of Lemma fix-corec-partial1


1. A : Type
2. value-type(A)
3. mono(A)
4. F : Type ⟶ Type
5. f : (corec(T.F[T]) ⟶ partial(A)) ⟶ corec(T.F[T]) ⟶ partial(A)
6. x : corec(T.F[T])
⊢ fix(f) x ∈ partial(A)
BY
{ (InstLemma `fixpoint-induction-bottom2` [⌜A⌝;⌜corec(T.F[T]) ⟶ partial(A)⌝;⌜λ2f.f x⌝;⌜f⌝]⋅ THEN Auto) }

---

Latex:

---

Latex:

1.  A  :  Type
2.  value-type(A)
3.  mono(A)
4.  F  :  Type  {}\mrightarrow{}  Type
5.  f  :  (corec(T.F[T])  {}\mrightarrow{}  partial(A))  {}\mrightarrow{}  corec(T.F[T])  {}\mrightarrow{}  partial(A)
6.  x  :  corec(T.F[T])
\mvdash{}  fix(f)  x  \mmember{}  partial(A)


By

---

Latex:
(InstLemma  `fixpoint-induction-bottom2`  [\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}corec(T.F[T])  {}\mrightarrow{}  partial(A)\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}f.f  x\mkleeneclose{};\mkleeneopen{}f\mkleeneclose{}]\mcdot{}
  THEN  Auto
  )

---

Home Index