---

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


1. P : ℙ
2. x : P@i
3. P@i
⊢ ↑[inl x]b
BY
{ (RepUR ``dcdr-to-bool assert ifthenelse`` 0 THEN Auto) }

---

Latex:

---

Latex:

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


By

---

Latex:
(RepUR  ``dcdr-to-bool  assert  ifthenelse``  0  THEN  Auto)

---

Home Index