Investigate potential bug in the filtering step of Dafny's trigger generation

[keyboardDrummer]

The IsStrongerThan method seems wrong because it will consider P(G(x)) to be stronger than P(x). Indeed, the former matches on strictly fewer patterns than the latter, but it will also produce different instantiations for x, so in that sense it is not stronger.

To reproduce, use:

method Bar() {
  assert forall x :: P(x) && P(G(x));
}

function P(x: bool): bool
function G(x: bool): bool