-
-(* notation < "|term 19 e|" non associative with precedence 70 for @{'forget $e}.*)
-interpretation "forget" 'norm a = (forget ? a).
+
+(* Already in the library
+notation "| term 19 C |" with precedence 70 for @{ 'card $C }.
+*)
+interpretation "forget" 'card a = (forget ? a).