---

Step * of Lemma oobleft_wf

∀[A,B:Type]. ∀[lval:A].  (oobleft(lval) ∈ one_or_both(A;B))
BY
{ Unfolds ``one_or_both oobleft`` 0 THEN Auto THEN MemTypeCD THEN Auto }

---

Latex:

---

Latex:
\mforall{}[A,B:Type].  \mforall{}[lval:A].    (oobleft(lval)  \mmember{}  one\_or\_both(A;B))


By

---

Latex:
Unfolds  ``one\_or\_both  oobleft``  0  THEN  Auto  THEN  MemTypeCD  THEN  Auto

---

Home Index