+
+notation "hvbox( h ⊢ break term 46 L1 ⊢ • ⊑ [ term 46 g ] break term 46 L2 )"
+ non associative with precedence 45
+ for @{ 'CrSubEqSE $h $g $L1 $L2 }.
+
+notation "hvbox( ⦃ term 46 L1 ⦄ ⬌ * break ⦃ term 46 L2 ⦄ )"
+ non associative with precedence 45
+ for @{ 'FocalizedPConvStar $L1 $L2 }.
+
+notation "hvbox( ⦃ term 46 L1 , break term 46 T1 ⦄ ⬌ * break ⦃ term 46 L2 , break term 46 T2 ⦄ )"
+ non associative with precedence 45
+ for @{ 'FocalizedPConvStar $L1 $T1 $L2 $T2 }.
+
+notation "hvbox( ⦃ term 46 L1 ⦄ ⬌ ⬌ * break ⦃ term 46 L2 ⦄ )"
+ non associative with precedence 45
+ for @{ 'FocalizedPConvStarAlt $L1 $L2 }.
+
+notation "hvbox( ⦃ term 46 L1 , break term 46 T1 ⦄ ⬌ ⬌ * break ⦃ term 46 L2 , break term 46 T2 ⦄ )"
+ non associative with precedence 45
+ for @{ 'FocalizedPConvStarAlt $L1 $T1 $L2 $T2 }.
+
+(* Dynamic typing ***********************************************************)
+
+notation "hvbox( ⦃ term 46 h , break term 46 L ⦄ ⊩ break term 46 T : break [ term 46 g ] )"
+ non associative with precedence 45
+ for @{ 'NativeValid $h $g $L $T }.
+
+notation "hvbox( h ⊢ break term 46 L1 ⊩ : ⊑ [ term 46 g ] break term 46 L2 )"
+ non associative with precedence 45
+ for @{ 'CrSubEqV $h $g $L1 $L2 }.
+
+notation "hvbox( ⦃ term 46 h , break term 46 L ⦄ ⊢ break term 46 T1 : break term 46 T2 )"
+ non associative with precedence 45
+ for @{ 'NativeType $h $L $T1 $T2 }.
+
+notation "hvbox( ⦃ term 46 h , break term 46 L ⦄ ⊢ break term 46 T1 : : break term 46 T2 )"
+ non associative with precedence 45
+ for @{ 'NativeTypeAlt $h $L $T1 $T2 }.
+
+(* Higher order dynamic typing **********************************************)
+
+notation "hvbox( ⦃ term 46 h , break term 46 L ⦄ ⊢ break term 46 T1 : * break term 46 T2 )"
+ non associative with precedence 45
+ for @{ 'NativeTypeStar $h $L $T1 $T2 }.