---

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


1. [P] : ℙ
2. y : ¬P@i
3. ↑[inr y ]b@i
⊢ P
BY
{ ( Unfold `dcdr-to-bool` (-1) THEN Reduce (-1)) }

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

---

Latex:

---

Latex:

1.  [P]  :  \mBbbP{}
2.  y  :  \mneg{}P@i
3.  \muparrow{}[inr  y  ]\msubb{}@i
\mvdash{}  P


By

---

Latex:
(  Unfold  `dcdr-to-bool`  (-1)  THEN  Reduce  (-1))

---

Home Index