---

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


1. [P] : ℙ
2. y : ¬P@i
3. ↑(inr ⋅ )@i
⊢ P
BY
{ (RepUR ``assert ifthenelse`` -1 THEN Auto) }

---

Latex:

---

Latex:

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


By

---

Latex:
(RepUR  ``assert  ifthenelse``  -1  THEN  Auto)

---

Home Index