Possible redesign of handling of persistent/intuitionistic propositions in intro patterns

At !370 (comment 43784) we had some discussion about possible re-designs of the handling of persistent/intuitionistic propositions (when # is needed and when not) with the goal of being more consistent. That was put on hold for now due to being too much work and likely also breaking many things; the issue here tracks possibly doing at least some of that in the future if we want to improve the situation around the # pattern (and its opt-out version, whatever that will be).