---

Step * 1 of Lemma decidable__ex_unit

.....decidable?..... 
1. [P] : Unit ─→ ℙ
2. Dec(P[⋅])@i
3. x : Unit@i
⊢ Dec(P[x])
BY
{ ((D (-1)) THEN Fold `it` 0 THEN Auto) }

---

Latex:


.....decidable?..... 
1.  [P]  :  Unit  {}\mrightarrow{}  \mBbbP{}
2.  Dec(P[\mcdot{}])@i
3.  x  :  Unit@i
\mvdash{}  Dec(P[x])


By

((D  (-1))  THEN  Fold  `it`  0  THEN  Auto)

---

Home Index