+ for @{ 'FocalizedPRed $L1 $L2 }.
+
+notation "hvbox( ⦃ L1, break T1 ⦄ ➡ break ⦃ L2 , break T2 ⦄ )"
+ non associative with precedence 45
+ for @{ 'FocalizedPRed $L1 $T1 $L2 $T2 }.
+
+notation "hvbox( L ⊢ break ⦃ L1, break T1 ⦄ ➡ break ⦃ L2 , break T2 ⦄ )"
+ non associative with precedence 45
+ for @{ 'FocalizedPRed $L $L1 $T1 $L2 $T2 }.
+
+notation "hvbox( ⦃ L1 ⦄ ➡ ➡ break ⦃ L2 ⦄ )"
+ non associative with precedence 45
+ for @{ 'FocalizedPRedAlt $L1 $L2 }.
+
+notation "hvbox( ⦃ h , break L ⦄ ⊢ break term 46 T1 • ➡ break [ g ] break term 46 T2 )"
+ non associative with precedence 45
+ for @{ 'XPRed $h $g $L $T1 $T2 }.
+
+notation "hvbox( h ⊢ break ⦃ L1, break T1 ⦄ • ⥸ break [ g ] break ⦃ L2 , break T2 ⦄ )"
+ non associative with precedence 45
+ for @{ 'YPRed $h $g $L1 $T1 $L2 $T2 }.