---

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