---

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


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

1
1. P : ℙ
2. x : P@i
3. P@i
⊢ ↑[inl x]b

2
1. P : ℙ
2. y : ¬P@i
3. P@i
⊢ ↑[inr y ]b

---

Latex:

---

Latex:

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


By

---

Latex:
(Unfolds  ``decidable``  2  THEN  D  -2)

---

Home Index