---

Step * of Lemma oobright_wf

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

---

Latex:

---

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


By

---

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

---

Home Index