---

Step * of Lemma oobleft-lval_wf

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

---

Latex:

---

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


By

---

Latex:
DatatypeSelectorWf  ``oobboth  oobleft  oobright``

---

Home Index