---

Step * of Lemma unique-corec-solution

∀[F:Type ⟶ Type]
  ∀[I:Type]
    ∀G:⋂T:{T:Type| (F[T] ⊆r T) ∧ (corec(T.F[T]) ⊆r T)} . ((I ⟶ T) ⟶ I ⟶ F[T])
      ∃!s:I ⟶ corec(T.F[T]). (s = (G s) ∈ (I ⟶ corec(T.F[T]))) 
  supposing ContinuousMonotone(T.F[T])
BY
{ TACTIC:(Auto
          THEN (InstLemma `corec-ext` [⌜F⌝]⋅ THENA Auto)
          THEN D -1
          THEN (Assert ⌜G ∈ (I ⟶ corec(T.F[T])) ⟶ I ⟶ corec(T.F[T])⌝⋅
                THENA (SubsumeC ⌜(I ⟶ corec(T.F[T])) ⟶ I ⟶ F[corec(T.F[T])]⌝⋅ THEN Auto)
                )) }

1
1. [F] : Type ⟶ Type
2. ContinuousMonotone(T.F[T])
3. [I] : Type
4. G : ⋂T:{T:Type| (F[T] ⊆r T) ∧ (corec(T.F[T]) ⊆r T)} . ((I ⟶ T) ⟶ I ⟶ F[T])
5. corec(T.F[T]) ⊆r F[corec(T.F[T])]
6. F[corec(T.F[T])] ⊆r corec(T.F[T])
7. G ∈ (I ⟶ corec(T.F[T])) ⟶ I ⟶ corec(T.F[T])
⊢ ∃!s:I ⟶ corec(T.F[T]). (s = (G s) ∈ (I ⟶ corec(T.F[T])))

---

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])
            \mexists{}!s:I  {}\mrightarrow{}  corec(T.F[T]).  (s  =  (G  s)) 
    supposing  ContinuousMonotone(T.F[T])


By

---

Latex:
TACTIC:(Auto
                THEN  (InstLemma  `corec-ext`  [\mkleeneopen{}F\mkleeneclose{}]\mcdot{}  THENA  Auto)
                THEN  D  -1
                THEN  (Assert  \mkleeneopen{}G  \mmember{}  (I  {}\mrightarrow{}  corec(T.F[T]))  {}\mrightarrow{}  I  {}\mrightarrow{}  corec(T.F[T])\mkleeneclose{}\mcdot{}
                            THENA  (SubsumeC  \mkleeneopen{}(I  {}\mrightarrow{}  corec(T.F[T]))  {}\mrightarrow{}  I  {}\mrightarrow{}  F[corec(T.F[T])]\mkleeneclose{}\mcdot{}  THEN  Auto)
                            ))

---

Home Index