---

Step * of Lemma oobboth-bval_wf

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

---

Latex:

---

Latex:
No  Annotations
\mforall{}[A,B:Type].  \mforall{}[x:one\_or\_both(A;B)].    oobboth-bval(x)  \mmember{}  A  \mtimes{}  B  supposing  \muparrow{}oobboth?(x)


By

---

Latex:
DatatypeSelectorWf  ``oobboth  oobleft  oobright``

---

Home Index