+ for @{'Subst $M $l}.
+
+notation "hvbox(M break [ k ≝ N ])"
+ non associative with precedence 90
+ for @{'Subst1 $M $k $N}.
+
+(* type judgements *)
+
+notation "hvbox(G break ⊢ A break : B)"
+ non associative with precedence 45
+ for @{'TJ $G $A $B}.
+
+notation "hvbox(G break ⊢ A break ÷ B)"
+ non associative with precedence 45
+ for @{'TJ0 $G $A $B}.
+
+(* interpretations *)
+
+notation "hvbox(║T║)"
+ non associative with precedence 55
+ for @{'IInt $T}.
+
+notation "hvbox(║T║ break _ [E])"
+ non associative with precedence 55
+ for @{'IInt1 $T $E}.
+
+notation "hvbox(║T║ break _ [E1 break , E2])"
+ non associative with precedence 55
+ for @{'IInt2 $T $E1 $E2}.
+
+notation "hvbox(║T║ * break _ [E])"
+ non associative with precedence 55
+ for @{'IIntS1 $T $E}.
+
+notation "hvbox(〚T〛)"
+ non associative with precedence 55
+ for @{'EInt $T}.
+
+notation "hvbox(〚T〛 break _ [E])"
+ non associative with precedence 55
+ for @{'EInt1 $T $E}.
+
+notation "hvbox(〚T〛 break _ [E1 break , E2])"
+ non associative with precedence 55
+ for @{'EInt2 $T $E1 $E2}.
+
+notation "hvbox(《T》)"
+ non associative with precedence 55
+ for @{'XInt $T}.