---

Step * of Lemma decidable__assert

∀b:𝔹. Dec(↑b)
BY
{ ((D 0 THENA Auto)
   THEN UseWitness ⌜case b of inl(x) => inl x | inr(x) => inr (λx.Ax) ⌝⋅
   THEN D -1
   THEN RepUR ``decidable or not assert ifthenelse`` 0
   THEN Auto
   THEN D 1
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}b:\mBbbB{}.  Dec(\muparrow{}b)


By

---

Latex:
((D  0  THENA  Auto)
  THEN  UseWitness  \mkleeneopen{}case  b  of  inl(x)  =>  inl  x  |  inr(x)  =>  inr  (\mlambda{}x.Ax)  \mkleeneclose{}\mcdot{}
  THEN  D  -1
  THEN  RepUR  ``decidable  or  not  assert  ifthenelse``  0
  THEN  Auto
  THEN  D  1
  THEN  Auto)

---

Home Index