Add lemma `intuitionistically_def P : □ P = <affine> <pers> P`.
This is just the definition. One direction can be obtained by unfolding, but in proofs it is sometimes useful to "fold", i.e., go the other direction. That can be done with this lemma.
This is just the definition. One direction can be obtained by unfolding, but in proofs it is sometimes useful to "fold", i.e., go the other direction. That can be done with this lemma.