notation "hvbox (r \sub \c)" with precedence 90 for @{'concr_rel $r}.
notation "hvbox (r \sub \f)" with precedence 90 for @{'form_rel $r}.
+
+notation < "mstyle color #ff0000 (…)" non associative with precedence 90
+for @{'hide}.
+
+definition hide ≝ λA:Type.λx:A.x.
+
+interpretation "hide" 'hide = (hide _ _).