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