---

Step * of Lemma dcdr-to-bool-equivalence

∀[P:ℙ]. ∀d:Dec(P). (↑[d]b ⇐⇒ P)
BY
{ Auto }

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

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

---

Latex:

---

Latex:
\mforall{}[P:\mBbbP{}].  \mforall{}d:Dec(P).  (\muparrow{}[d]\msubb{}  \mLeftarrow{}{}\mRightarrow{}  P)


By

---

Latex:
Auto

---

Home Index