---

Step * of Lemma CCC-finite

∀[T:Type]. (finite(T) ⇒ CCC(T))
BY
{ (Auto THEN D -1 THEN Assert ⌜CCC(ℕn)⌝⋅) }

1
.....assertion..... 
1. [T] : Type
2. n : ℕ
3. T ~ ℕn
⊢ CCC(ℕn)

2
1. [T] : Type
2. n : ℕ
3. T ~ ℕn
4. CCC(ℕn)
⊢ CCC(T)

---

Latex:

---

Latex:
\mforall{}[T:Type].  (finite(T)  {}\mRightarrow{}  CCC(T))


By

---

Latex:
(Auto  THEN  D  -1  THEN  Assert  \mkleeneopen{}CCC(\mBbbN{}n)\mkleeneclose{}\mcdot{})

---

Home Index