Make proof search for contradictions more aggressive?

[ghost]

This one may be asking a bit much:

The goal is False, Knight B is a hypothesis, and there's a nice, juicy contradiction bi-implied by it. This case is especially frustrating because we get a useless suggestion of apply C_says in H. when it's really apply B_says in H. we want, and if we try it, a) it works, b) the remainder of the proof continues to be point-and-click. :-)