---

Step * of Lemma derived-seq_wf

∀[T:Type]. ∀[f:ℕ ⟶ T]. ∀[s:k:ℕ × (ℕk ⟶ ℕ)].  (derived-seq(f;s) ∈ ℕ ⟶ (k:ℕ × (ℕk ⟶ T)))
BY
{ xxx(Unfold `derived-seq` 0 THEN Auto')xxx }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[f:\mBbbN{}  {}\mrightarrow{}  T].  \mforall{}[s:k:\mBbbN{}  \mtimes{}  (\mBbbN{}k  {}\mrightarrow{}  \mBbbN{})].    (derived-seq(f;s)  \mmember{}  \mBbbN{}  {}\mrightarrow{}  (k:\mBbbN{}  \mtimes{}  (\mBbbN{}k  {}\mrightarrow{}  T)))


By

---

Latex:
xxx(Unfold  `derived-seq`  0  THEN  Auto')xxx

---

Home Index