Step
*
of Lemma
firstn-mklist1
∀[m,n:ℕ]. ∀[f:ℕm ⟶ Top].  ((n ≤ m) 
⇒ (firstn(n;mklist(m;f)) ~ mklist(n;f)))
BY
{ Auto }
1
1. m : ℕ
2. n : ℕ
3. f : ℕm ⟶ Top
4. n ≤ m
⊢ firstn(n;mklist(m;f)) ~ mklist(n;f)
Latex:
Latex:
\mforall{}[m,n:\mBbbN{}].  \mforall{}[f:\mBbbN{}m  {}\mrightarrow{}  Top].    ((n  \mleq{}  m)  {}\mRightarrow{}  (firstn(n;mklist(m;f))  \msim{}  mklist(n;f)))
By
Latex:
Auto
Home
Index