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).