better drop background syntax if entity depends on parameters; more direct Type_Infer_Context.const_type instead of Syntax.check_term, which expands abbreviations (and potentially more);

more uniform abbrev vs. define;

tuned;