---

Step * of Lemma fix_wf_corec-alt-proof

∀[F:Type ⟶ Type]. ∀[G:⋂T:Type. (T ⟶ F[T])].  (fix(G) ∈ corec(T.F[T]))
BY
{ (Auto
   THEN Subst' fix(G) ~ (λG.fix(G)) G 0
   THEN Try ((Reduce 0 THEN Trivial))
   THEN GenConclAtAddrType ⋂F:{F:ℕ ⟶ Type| Top ⊆r (F 0)} . ((⋂n:ℕ. ((F n) ⟶ (F (n + 1)))) ⟶ (⋂n:ℕ. (F n))) [2;1]⋅
   THEN Try (Complete (Auto))) }

---

Latex:

---

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


By

---

Latex:
(Auto
  THEN  Subst'  fix(G)  \msim{}  (\mlambda{}G.fix(G))  G  0
  THEN  Try  ((Reduce  0  THEN  Trivial))
  THEN  GenConclAtAddrType  \mcap{}F:\{F:\mBbbN{}  {}\mrightarrow{}  Type|  Top  \msubseteq{}r  (F  0)\} 
                                                      ((\mcap{}n:\mBbbN{}.  ((F  n)  {}\mrightarrow{}  (F  (n  +  1))))  {}\mrightarrow{}  (\mcap{}n:\mBbbN{}.  (F  n)))  [2;1]\mcdot{}
  THEN  Try  (Complete  (Auto)))

---

Home Index