Step
*
1
1
1
1
of Lemma
listify_length
1. T : Type
2. n : ℤ
⊢ ∀m:{...n}. ∀f:{m..n-} ⟶ T. (||listify(f;m;n)|| = (n - m) ∈ ℤ)
BY
{ ((BLemma `int_lower_ind` THENM UnivCD) THENA Auto) }
1
1. T : Type
2. n : ℤ
3. f : {n..n-} ⟶ T
⊢ ||listify(f;n;n)|| = (n - n) ∈ ℤ
2
1. T : Type
2. n : ℤ
3. m : {...n - 1}
4. ∀f:{m + 1..n-} ⟶ T. (||listify(f;m + 1;n)|| = (n - m + 1) ∈ ℤ)
5. f : {m..n-} ⟶ T
⊢ ||listify(f;m;n)|| = (n - m) ∈ ℤ
Latex:
Latex:
1. T : Type
2. n : \mBbbZ{}
\mvdash{} \mforall{}m:\{...n\}. \mforall{}f:\{m..n\msupminus{}\} {}\mrightarrow{} T. (||listify(f;m;n)|| = (n - m))
By
Latex:
((BLemma `int\_lower\_ind` THENM UnivCD) THENA Auto)
Home
Index