When having H : ▷ (P -∗ Q) and H2 : ▷ P, iSpecialize ("H" with "H2")
distributes the later over the wand.