Variant of Search(About) that allows declaring some constants equivalent

[coqbot]

Note: the issue was created automatically with bugzilla2github tool

Original bug ID: BZ#3904
From: @JasonGross
Reported version: trunk
CC: coq-bugs-redist@lists.gforge.inria.fr

[coqbot]

Comment author: @JasonGross

There should be a variant of SearchAbout that works up to unfolding (or substitution, perhaps, if it's uconstr-based) of particular terms. Much like there is now [Declare Equivalent Keys] for keyed unification, there should be [Declare Equivalent Search Terms] or similar, so that if I have [Definition Foo x := Bar (f x)], and I [Declare Equivalent Search Terms Foo Bar], then [SearchAbout (Foo _ -> Foo _ -> nat)] will also tell me about theorems of type [Bar (f _) -> Foo _ -> nat], [Bar (f _) -> Bar (f _) -> nat], etc. (It would not be terrible if it told me about theorems of the form [Bar _ -> Bar _ -> nat], too, instead of just [Bar (f _)] ones.)