- Allow framing of persistent hypotheses below the always modality.
- Allow framing of persistent hypotheses in just one branch of a
  disjunction.