-non associative with precedence 50 for @{ 'bigcup_mk (λ${ident i}:$I.$p) }.
-notation > "hovbox(⋃ f)" non associative with precedence 60 for @{ 'bigcup $f }.
+non associative with precedence 55 for @{ 'bigcup_mk (λ${ident i}:$I.$p) }.
+notation > "hovbox(⋃ f)" non associative with precedence 65 for @{ 'bigcup $f }.