---

Step * of Lemma decidable__ex_unit

∀[P:Unit ─→ ℙ]. (Dec(P[⋅]) ⇒ Dec(∃x:Unit. P[x]))
BY
{ (Auto THEN BLemma `decidable-exists-finite` THEN Auto) }

1
.....decidable?..... 
1. [P] : Unit ─→ ℙ
2. Dec(P[⋅])@i
3. x : Unit@i
⊢ Dec(P[x])

---

Latex:


\mforall{}[P:Unit  {}\mrightarrow{}  \mBbbP{}].  (Dec(P[\mcdot{}])  {}\mRightarrow{}  Dec(\mexists{}x:Unit.  P[x]))


By

(Auto  THEN  BLemma  `decidable-exists-finite`  THEN  Auto)

---

Home Index