+notation "hvbox( L ⊢ break [ d , break e ] break 𝐑 [ T ] )"
+ non associative with precedence 45
+ for @{ 'Reducible $L $d $e $T }.
+
+notation "hvbox( L ⊢ break [ d , break e ] break 𝐈 [ T ] )"
+ non associative with precedence 45
+ for @{ 'NotReducible $L $d $e $T }.
+
+notation "hvbox( L ⊢ break [ d , break e ] break 𝐍 [ T ] )"
+ non associative with precedence 45
+ for @{ 'Normal $L $d $e $T }.
+
+notation "hvbox( ⇧ [ d , break e ] break T1 ≡ break T2 )"