Rename lemma `satisfied` to `any⇒satisfiable` in `*.Relation.Unary.Any`

[MatthewDaggitt]

See discussion in #2862 where @jamesmckinna makes this suggestion. I agree that it is a much better name.

Really the lemma that should be called satisfiable should be Satisfiable P -> Satisfiable (Any P). Of course the opposite lemma also holds Satisfiable (Any P) -> Satisfiable P so maybe the naming needs to be thought about more carefully.

[jamesmckinna]

Good to lift this out separately.
As with #2846 , the story is perhaps a bit trickier than meets the eye at first glance.

UPDATED: What I'm not clear about, following style-guide, is whether the above lemmas should be called

• any⁺ or satisfiable⁺
• any⁻ or satisfiable⁻
  ???

[jamesmckinna]

Having raised #2954 I've had time to rethink the naming scheme:

• satisfied/any⇒satisfiable is somehow the 'simplest' of the three lemmas (at least in terms of its type), and the prefix any⇒ feels redundant, given that that the module-level scope defines Any, and hence its potential 'observers' (in Meyer's terminology) are implicitly governed by such an outermost qualification... so I now think that the 'right'/'better' name should simply be satisfiable
• so what to do about the other examples which @MatthewDaggitt mentions? well, they involve the 'more complex' composition Satisfiable (Any ...), and our ambient naming idiom/heuristic for such compounds, for functions at least, is to run the two names together...; adding in the 'intro'/'elim' qualifiers in the form of superscript ⁺/⁻ leads me now to propose satisfiable-any⁺/satisfiable-any⁻ for intro/elim of the compound property.

UPDATED: latest commits on #2954 make a yet stronger choice for the second point: satisfiable⁺/satisfiable⁻

Comments welcome! (flame-hat on ;-))

[JacquesCarette]

Well, look at that, I commented in the same direction (redundancy) in the PR itself, before looking at this. I agree that satisfiable, especially in its Any.satisfiable guise, is a much better name.

At the moment, I'm fine with @jamesmckinna suggestions in the second point. But opinion not held strongly, could be swayed by other arguments.