definition lo ≝ λS:\ 5a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"\ 6DeqSet\ 5/a\ 6.λa,b:\ 5a href="cic:/matita/tutorial/chapter7/pre.def(1)"\ 6pre\ 5/a\ 6 S.\ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6〈\ 5/a\ 6\ 5a title="pair pi1" href="cic:/fakeuri.def(1)"\ 6\fst\ 5/a\ 6 a \ 5a title="pitem or" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6 \ 5a title="pair pi1" href="cic:/fakeuri.def(1)"\ 6\fst\ 5/a\ 6 b,\ 5a title="pair pi2" href="cic:/fakeuri.def(1)"\ 6\snd\ 5/a\ 6 a \ 5a title="boolean or" href="cic:/fakeuri.def(1)"\ 6∨\ 5/a\ 6 \ 5a title="pair pi2" href="cic:/fakeuri.def(1)"\ 6\snd\ 5/a\ 6 b〉.
notation "a ⊕ b" left associative with precedence 60 for @{'oplus $a $b}.
interpretation "oplus" 'oplus a b = (lo ? a b).
definition lo ≝ λS:\ 5a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"\ 6DeqSet\ 5/a\ 6.λa,b:\ 5a href="cic:/matita/tutorial/chapter7/pre.def(1)"\ 6pre\ 5/a\ 6 S.\ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6〈\ 5/a\ 6\ 5a title="pair pi1" href="cic:/fakeuri.def(1)"\ 6\fst\ 5/a\ 6 a \ 5a title="pitem or" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6 \ 5a title="pair pi1" href="cic:/fakeuri.def(1)"\ 6\fst\ 5/a\ 6 b,\ 5a title="pair pi2" href="cic:/fakeuri.def(1)"\ 6\snd\ 5/a\ 6 a \ 5a title="boolean or" href="cic:/fakeuri.def(1)"\ 6∨\ 5/a\ 6 \ 5a title="pair pi2" href="cic:/fakeuri.def(1)"\ 6\snd\ 5/a\ 6 b〉.
notation "a ⊕ b" left associative with precedence 60 for @{'oplus $a $b}.
interpretation "oplus" 'oplus a b = (lo ? a b).