---

Step * of Lemma fix_wf_corec_system

∀[F:Type ⟶ Type]
  ∀[I:Type]. ∀[G:⋂T:{T:Type| (F[T] ⊆r T) ∧ (corec(T.F[T]) ⊆r T)} . ((I ⟶ T) ⟶ I ⟶ F[T])].
    (fix(G) ∈ I ⟶ corec(T.F[T])) 
  supposing Monotone(T.F[T])
BY
{ TACTIC:(Auto THEN Using [`H',⌜λ2T.I ⟶ T⌝;`F',⌜F⌝] (BLemma `fix_wf_corec1`)⋅ THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[F:Type  {}\mrightarrow{}  Type]
    \mforall{}[I:Type].  \mforall{}[G:\mcap{}T:\{T:Type|  (F[T]  \msubseteq{}r  T)  \mwedge{}  (corec(T.F[T])  \msubseteq{}r  T)\}  .  ((I  {}\mrightarrow{}  T)  {}\mrightarrow{}  I  {}\mrightarrow{}  F[T])].
        (fix(G)  \mmember{}  I  {}\mrightarrow{}  corec(T.F[T])) 
    supposing  Monotone(T.F[T])


By

---

Latex:
TACTIC:(Auto  THEN  Using  [`H',\mkleeneopen{}\mlambda{}\msubtwo{}T.I  {}\mrightarrow{}  T\mkleeneclose{};`F',\mkleeneopen{}F\mkleeneclose{}]  (BLemma  `fix\_wf\_corec1`)\mcdot{}  THEN  Auto)

---

Home Index