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