For example, when having `H : ▷ P → Q` and `HP : P`, we can now do `iSpecialize ("H" with "HP")`. This is achieved by putting a `FromAssumption` premise in the base instance for `IntoWand`.
