Allow framing below an modality if the hypothesis that is framed is affine. (Previously, framing below was only possible if the hypothesis that is framed resides in the intuitionistic context.)
This is part (1) of !450 (closed). See !521 (merged) for a discussion why we don't want the rest of that MR.