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 _ _).
+interpretation "hide" 'hide x = (hide ? x).