---

Step * of Lemma oobboth_wf

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

---

Latex:

---

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


By

---

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

---

Home Index