The problem scope of proof automation is large and there are many design decisions to do. Coming from the particular field of low-level semantics and verification and from our experience in other proof assistant ecosystems, we came to the conclusion that the Coq ecosystem lacks a general white-box proof search engines such as the fastforce family of tactics in Isabelle or aesop in Lean. To our knowledge, the sauto tactic from CoqHammer is the closest instance of that in the Coq ecosystem, but it is still lacking some extensibility to be truly usable. In response, we have started designing an important phase of what such a proof search could look like: cdestruct, a context cleaner or normalizer, that tries to simplify a proof context purely using user specified hints, in the hope that it can be later extended to a larger scope.