---

Step * of Lemma fix_wf_corec2

∀[F,H:Type ⟶ Type].
  ∀[G:⋂T:Type. (H[T] ⟶ H[F[T]]) ⋂ Top ⟶ H[Top]]. (fix(G) ∈ H[corec(T.F[T])]) supposing Continuous(T.H[T])
BY
{ ((InstLemma Obid: fix_wf_corec2') []⋅ THEN RepeatFor 4 (ParallelLast') THEN DoSubsume THEN Try (Complete (Auto))) }

---

Latex:

---

Latex:
\mforall{}[F,H:Type  {}\mrightarrow{}  Type].
    \mforall{}[G:\mcap{}T:Type.  (H[T]  {}\mrightarrow{}  H[F[T]])  \mcap{}  Top  {}\mrightarrow{}  H[Top]].  (fix(G)  \mmember{}  H[corec(T.F[T])]) 
    supposing  Continuous(T.H[T])


By

---

Latex:
((InstLemma  Obid:  fix\_wf\_corec2')  []\mcdot{}
  THEN  RepeatFor  4  (ParallelLast')
  THEN  DoSubsume
  THEN  Try  (Complete  (Auto)))

---

Home Index