Maybe it would be better if all local definitions were done with `Let` insetad of `Definition`. That way we do not pollute the rest of the file. (And each entry is supposed to be independent of the others  if possible.)