Merge branch 'robbert/intuitionistically_intro' into 'master'

Generalize `intuitionistically_intro` to general BI.

See merge request iris/iris!911

iris/bi/derived_laws.v

@@ -1632,14 +1632,12 @@ would be its only field. *)
 Lemma intuitionistic P `{!Persistent P, !Affine P} : P ⊢ □ P.
 Proof. rewrite intuitionistic_intuitionistically. done. Qed.
 
+Lemma intuitionistically_intro P Q `{!Affine P, !Persistent P} : (P ⊢ Q) → P ⊢ □ Q.
+Proof. intros. apply: affinely_intro. by apply: persistently_intro. Qed.
+
 Section persistent_bi_absorbing.
   Context `{!BiAffine PROP}.
 
-  Lemma intuitionistically_intro P Q `{!Persistent P} : (P ⊢ Q) → P ⊢ □ Q.
-  Proof.
-    intros HP. rewrite (persistent P) HP intuitionistically_into_persistently //.
-  Qed.
-
   Lemma persistent_and_sep P Q `{HPQ : !TCOr (Persistent P) (Persistent Q)} :
     P ∧ Q ⊣⊢ P ∗ Q.
   Proof.