+(* Reducibility *************************************************************)
+
+notation "hvbox( โ [ T ] )"
+ non associative with precedence 45
+ for @{ 'Reducible $T }.
+
+notation "hvbox( L โข โ [ T ] )"
+ non associative with precedence 45
+ for @{ 'Reducible $L $T }.
+
+notation "hvbox( ๐ [ T ] )"
+ non associative with precedence 45
+ for @{ 'NotReducible $T }.
+
+notation "hvbox( L โข ๐ [ T ] )"
+ non associative with precedence 45
+ for @{ 'NotReducible $L $T }.
+
+notation "hvbox( โ [ T ] )"
+ non associative with precedence 45
+ for @{ 'Normal $T }.
+
+notation "hvbox( L โข โ [ T ] )"
+ non associative with precedence 45
+ for @{ 'Normal $L $T }.