---

Step * of Lemma oobright-rval_wf

∀[A,B:Type]. ∀[x:one_or_both(A;B)].  oobright-rval(x) ∈ B supposing ↑oobright?(x)
BY
{ DatatypeSelectorWf `` oobboth oobleft oobright`` }

---

Latex:

---

Latex:
\mforall{}[A,B:Type].  \mforall{}[x:one\_or\_both(A;B)].    oobright-rval(x)  \mmember{}  B  supposing  \muparrow{}oobright?(x)


By

---

Latex:
DatatypeSelectorWf  ``  oobboth  oobleft  oobright``

---

Home Index