coercion cic:/matita/dama/sequence/fun_of_seq.con 1.
-notation < "hvbox((\lfloor p \rfloor) \sub ident i)"
- left associative with precedence 70
+notation < "hvbox((\lfloor term 19 p \rfloor) \sub ident i)" with precedence 90
for @{ 'sequence (\lambda ${ident i} : $t . $p)}.
-notation > "hvbox(\lfloor ident i, p \rfloor)"
- left associative with precedence 70
+notation > "hvbox((\lfloor term 19 p \rfloor) \sub ident i)" with precedence 90
+for @{ 'sequence (\lambda ${ident i} . $p)}.
+
+notation > "hvbox(\lfloor ident i, term 19 p \rfloor)" with precedence 90
for @{ 'sequence (\lambda ${ident i} . $p)}.
-notation "a \sub i" left associative with precedence 70
+notation "a \sub i" left associative with precedence 90
for @{ 'sequence_appl $a $i }.
interpretation "sequence" 'sequence \eta.x = (mk_seq _ x).