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