---

Step * of Lemma oob-getright_wf

∀[B,A:Type]. ∀[x:{x:one_or_both(A;B)| ↑oob-hasright(x)} ].  (oob-getright(x) ∈ B)
BY
{ ProveWfLemma }

1
1. B : Type
2. A : Type
3. x : one_or_both(A;B)
4. ↑oob-hasright(x)
5. ¬↑oobright?(x)
⊢ ↑oobboth?(x)

---

Latex:

---

Latex:
\mforall{}[B,A:Type].  \mforall{}[x:\{x:one\_or\_both(A;B)|  \muparrow{}oob-hasright(x)\}  ].    (oob-getright(x)  \mmember{}  B)


By

---

Latex:
ProveWfLemma

---

Home Index