---

Step * of Lemma oob-getleft_wf

∀[B,A:Type]. ∀[x:{x:one_or_both(A;B)| ↑oob-hasleft(x)} ].  (oob-getleft(x) ∈ A)
BY
{ xxxProveWfLemmaxxx }

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

---

Latex:

---

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


By

---

Latex:
xxxProveWfLemmaxxx

---

Home Index