simplified -- avoid odd mutable state, which potentially causes problems with module initialization;

back to static Mixfix.default_constraint without any special tricks (reverting e6443edaebff);

Type_Infer.object_logic controls improvement of type inference result;

tuned;

simplified constraints;

back to dummy constraints (amending dd2914250ca7): important for Syntax_Phases.get_free/is_declared;

tuned imports;

tuned message;

tuned;

added lemmas