---

Step * of Lemma m-corec_wf

∀[k:ℕ]. ∀[F:(ℕk ⟶ Type) ⟶ ℕk ⟶ Type]. ∀[i:ℕk].  (m-corec(T.F[T];i) ∈ Type)
BY
{ (ProveWfLemma THEN InstLemma `mutual-corec_wf` [⌜k⌝;⌜F⌝]⋅ THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[k:\mBbbN{}].  \mforall{}[F:(\mBbbN{}k  {}\mrightarrow{}  Type)  {}\mrightarrow{}  \mBbbN{}k  {}\mrightarrow{}  Type].  \mforall{}[i:\mBbbN{}k].    (m-corec(T.F[T];i)  \mmember{}  Type)


By

---

Latex:
(ProveWfLemma  THEN  InstLemma  `mutual-corec\_wf`  [\mkleeneopen{}k\mkleeneclose{};\mkleeneopen{}F\mkleeneclose{}]\mcdot{}  THEN  Auto)

---

Home Index