qed.
definition lo ≝ λS:DeqSet.λa,b:pre S.〈\fst a + \fst b,\snd a ∨ \snd b〉.
-notation "a ⊕ b" left associative with precedence 60 for @{'oplus $a $b}.
+notation "a ⊕ b" left associative with precedence 65 for @{'oplus $a $b}.
interpretation "oplus" 'oplus a b = (lo ? a b).
lemma lo_def: ∀S.∀i1,i2:pitem S.∀b1,b2. 〈i1,b1〉⊕〈i2,b2〉=〈i1+i2,b1∨b2〉.
definition pre_concat_r ≝ λS:DeqSet.λi:pitem S.λe:pre S.
match e with [ mk_Prod i1 b ⇒ 〈i · i1, b〉].
-notation "i ◃ e" left associative with precedence 60 for @{'lhd $i $e}.
+notation "i ◃ e" left associative with precedence 65 for @{'lhd $i $e}.
interpretation "pre_concat_r" 'lhd i e = (pre_concat_r ? i e).
lemma eq_to_ex_eq: ∀S.∀A,B:word S → Prop.
]
].
-notation "a ▹ b" left associative with precedence 60 for @{'tril eclose $a $b}.
+notation "a ▹ b" left associative with precedence 65 for @{'tril eclose $a $b}.
interpretation "item-pre concat" 'tril op a b = (pre_concat_l ? op a b).
-notation "•" non associative with precedence 60 for @{eclose ?}.
+notation "•" non associative with precedence 65 for @{eclose ?}.
let rec eclose (S: DeqSet) (i: pitem S) on i : pre S ≝
match i with
| pc i1 i2 ⇒ •i1 ▹ i2
| pk i ⇒ 〈(\fst (•i))^*,true〉].
-notation "• x" non associative with precedence 60 for @{'eclose $x}.
+notation "• x" non associative with precedence 65 for @{'eclose $x}.
interpretation "eclose" 'eclose x = (eclose ? x).
lemma eclose_plus: ∀S:DeqSet.∀i1,i2:pitem S.