---

Step * of Lemma finite-decidable-inhabited

∀[T:Type]. (finite(T) ⇒ (T ∨ (¬T)))
BY
{ (Auto
   THEN RepeatFor 2 (D -1)
   THEN (CaseNat 0 `n' THENL [((OrRight THEN Auto) THEN (D 0 THENA Auto)); (OrLeft THEN Auto)])) }

1
1. [T] : Type
2. n : ℕ
3. f : T ⟶ ℕn
4. Bij(T;ℕn;f)
5. n = 0 ∈ ℤ
6. T
⊢ False

2
1. [T] : Type
2. n : ℕ
3. f : T ⟶ ℕn
4. Bij(T;ℕn;f)
5. ¬(n = 0 ∈ ℤ)
⊢ T

---

Latex:

---

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


By

---

Latex:
(Auto
  THEN  RepeatFor  2  (D  -1)
  THEN  (CaseNat  0  `n'  THENL  [((OrRight  THEN  Auto)  THEN  (D  0  THENA  Auto));  (OrLeft  THEN  Auto)]))

---

Home Index