---

Step * of Lemma oob-left-or-right

∀[B,A:Type].  ∀x:one_or_both(A;B). ((↑oob-hasleft(x)) ∨ (↑oob-hasright(x)))
BY
{ (Auto THEN MoveToConcl (-1) THEN BLemma `one_or_both-induction` THEN RepUR ``oob-hasleft oob-hasright`` 0 THEN Auto) }

---

Latex:

---

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


By

---

Latex:
(Auto
  THEN  MoveToConcl  (-1)
  THEN  BLemma  `one\_or\_both-induction`
  THEN  RepUR  ``oob-hasleft  oob-hasright``  0
  THEN  Auto)

---

Home Index