---

Step * 1 of Lemma dcdr-to-bool-equivalence


1. [P] : ℙ
2. d : Dec(P)@i
3. ↑[d]b@i
⊢ P
BY
{ Unfold `decidable` 2 }

1
1. [P] : ℙ
2. d : P ∨ (¬P)@i
3. ↑[d]b@i
⊢ P

---

Latex:

---

Latex:

1.  [P]  :  \mBbbP{}
2.  d  :  Dec(P)@i
3.  \muparrow{}[d]\msubb{}@i
\mvdash{}  P


By

---

Latex:
Unfold  `decidable`  2

---

Home Index