Bring back side-conditionals for `iMod`

By @jtassaro

So, in Iris 2.0, if I'm recalling correctly, one only had (|={E1,E2}=> |={E2,E3}=> P) ={E1,E3}=> P under the assumption that E2 ⊆ E1 ∪ E3. I guess in the Iris 3.0 this assumption is no longer needed anymore, and so this assumption is not part of the FUpdFacts (and I can't think of a way to jam it into the instance of ElimModal so that iMod will do the right thing). The problem is that the logic from our ESOP 2017 paper is based on Iris 2.0 style so I need this assumption. Any thoughts? Obviously I can just re-define a version of iMod that accounts for this additional hypothesis, but I'm wondering if there's a preferred way.