Step
*
1
of Lemma
finite-function-type-equality
1. k : ℕ
2. F : ℕk ⟶ Type
3. i : ℕk
⊢ F[i] = F[upto(k)[i]] ∈ Type
BY
{ xxx((EqCD THEN Auto) THEN EqTypeCD THEN Auto)xxx }
Latex:
Latex:
1.  k  :  \mBbbN{}
2.  F  :  \mBbbN{}k  {}\mrightarrow{}  Type
3.  i  :  \mBbbN{}k
\mvdash{}  F[i]  =  F[upto(k)[i]]
By
Latex:
xxx((EqCD  THEN  Auto)  THEN  EqTypeCD  THEN  Auto)xxx
Home
Index