---

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


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

---

Latex:

---

Latex:

1.  [P]  :  \mBbbP{}
2.  x  :  P@i
3.  \muparrow{}[inl  x]\msubb{}@i
\mvdash{}  P


By

---

Latex:
Auto

---

Home Index