---

Step * of Lemma member-decide-assert

∀[x:𝔹]. (if x then tt else inr (λx.⋅)  fi  ∈ Dec(↑x))
BY
{ (Auto THEN (RepUR ``btrue decidable assert`` 0 THEN Auto)⋅) }

---

Latex:

---

Latex:
\mforall{}[x:\mBbbB{}].  (if  x  then  tt  else  inr  (\mlambda{}x.\mcdot{})    fi    \mmember{}  Dec(\muparrow{}x))


By

---

Latex:
(Auto  THEN  (RepUR  ``btrue  decidable  assert``  0  THEN  Auto)\mcdot{})

---

Home Index