Step
*
of Lemma
one_or_both_ind_oobboth_lemma
∀right,left,both,bval:Top.
(one_or_both_ind(oobboth(bval);bval.both[bval];lval.left[lval];rval.right[rval]) ~ both[bval])
BY
{ (UnivCD THENA Auto) }
1
1. right : Top@i
2. left : Top@i
3. both : Top@i
4. bval : Top@i
⊢ one_or_both_ind(oobboth(bval);bval.both[bval];lval.left[lval];rval.right[rval]) ~ both[bval]
Latex:
Latex:
\mforall{}right,left,both,bval:Top.
(one\_or\_both\_ind(oobboth(bval);bval.both[bval];lval.left[lval];rval.right[rval]) \msim{} both[bval])
By
Latex:
(UnivCD THENA Auto)
Home
Index