---

Step * 1 1 of Lemma finite-type-implies-finite


1. [T] : Type
2. ∀x,y:T.  Dec(x = y ∈ T)@i
3. finite-type(T)@i
4. n : ℕ
5. ℕn ~ T
6. finite-type(T)
7. finite(ℕn) ⇐⇒ finite(T)
⊢ finite(ℕn)
BY
{ (BLemma `nsub_finite` THEN Auto) }

---

Latex:

---

Latex:

1.  [T]  :  Type
2.  \mforall{}x,y:T.    Dec(x  =  y)@i
3.  finite-type(T)@i
4.  n  :  \mBbbN{}
5.  \mBbbN{}n  \msim{}  T
6.  finite-type(T)
7.  finite(\mBbbN{}n)  \mLeftarrow{}{}\mRightarrow{}  finite(T)
\mvdash{}  finite(\mBbbN{}n)


By

---

Latex:
(BLemma  `nsub\_finite`  THEN  Auto)

---

Home Index