---

Step * of Lemma finite-type-implies-finite

∀[T:Type]. ((∀x,y:T.  Dec(x = y ∈ T)) ⇒ finite-type(T) ⇒ finite(T))
BY
{ (InstLemma `finite-type-equipollent` []
   THEN RepeatFor 2 ((ParallelLast' THENA Auto))
   THEN Auto
   THEN ThinTrivial
   THEN ExRepD) }

1
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)
⊢ finite(T)

---

Latex:

---

Latex:
\mforall{}[T:Type].  ((\mforall{}x,y:T.    Dec(x  =  y))  {}\mRightarrow{}  finite-type(T)  {}\mRightarrow{}  finite(T))


By

---

Latex:
(InstLemma  `finite-type-equipollent`  []
  THEN  RepeatFor  2  ((ParallelLast'  THENA  Auto))
  THEN  Auto
  THEN  ThinTrivial
  THEN  ExRepD)

---

Home Index