Step
*
of Lemma
finite-function-type-equality
∀[k:ℕ]. ∀[F:ℕk ⟶ Type]. ((i:ℕk ⟶ F[i]) = (i:ℕk ⟶ map(λi.F[i];upto(k))[i]) ∈ Type)
BY
{ xxx(Auto
THEN EqCD
THEN Auto
THEN RWO "map_select" 0
THEN Auto
THEN Reduce 0
THEN Try ((RWO "length_upto" 0 THEN Auto)))xxx }
1
1. k : ℕ
2. F : ℕk ⟶ Type
3. i : ℕk
⊢ F[i] = F[upto(k)[i]] ∈ Type
Latex:
Latex:
\mforall{}[k:\mBbbN{}]. \mforall{}[F:\mBbbN{}k {}\mrightarrow{} Type]. ((i:\mBbbN{}k {}\mrightarrow{} F[i]) = (i:\mBbbN{}k {}\mrightarrow{} map(\mlambda{}i.F[i];upto(k))[i]))
By
Latex:
xxx(Auto
THEN EqCD
THEN Auto
THEN RWO "map\_select" 0
THEN Auto
THEN Reduce 0
THEN Try ((RWO "length\_upto" 0 THEN Auto)))xxx
Home
Index