smarter iIntros for plainly modality
The following discussion from !71 (merged) should be addressed:
-
@jung started a discussion: (+1 comment) Would it be a good idea or not for
iIntros
to be able to do this without us having to applypersistently_impl_plainly
? To me, that looks very similar to how it pulls out universal quantifiers from below a box.