Wingman doesn't use synthesized evidence

[isovector]

The destruct tactic generates a pattern match, and pattern matching on GADT constructors can introduce evidence into scope. Right now, Wingman just ignores this evidence. #1549 lets us use this argument if the user wrote it, but right now the following will fail:

data X f = Monad f => X

fun1 :: X f -> a -> f a
fun1 = _

while

fun1 :: X f -> a -> f a
fun1 X = _

works just fine