---

Step * of Lemma decidable-exists-finite

∀[T:Type]. (finite(T) ⇒ (∀[P:T ⟶ ℙ]. ((∀t:T. Dec(P[t])) ⇒ Dec(∃t:T. P[t]))))
BY
{ (InstLemma `decidable-exists-finite-type` [] THEN RepeatFor 2 (ParallelLast') THEN Auto) }

1
.....antecedent..... 
1. [T] : Type
2. finite(T)
⊢ finite-type(T)

---

Latex:

---

Latex:
\mforall{}[T:Type].  (finite(T)  {}\mRightarrow{}  (\mforall{}[P:T  {}\mrightarrow{}  \mBbbP{}].  ((\mforall{}t:T.  Dec(P[t]))  {}\mRightarrow{}  Dec(\mexists{}t:T.  P[t]))))


By

---

Latex:
(InstLemma  `decidable-exists-finite-type`  []  THEN  RepeatFor  2  (ParallelLast')  THEN  Auto)

---

Home Index