Make iStartProof convert Coq universals into bi universals.

theories/proofmode/class_instances.v

@@ -1024,6 +1024,7 @@ Global Instance elim_modal_bupd_plain `{BUpdFacts PROP} P Q :
   Plain P → ElimModal (|==> P) P Q Q.
 Proof. intros. by rewrite /ElimModal bupd_plain wand_elim_r. Qed.
 
+(* AsValid *)
 Global Instance as_valid_valid {PROP : bi} (P : PROP) : AsValid0 (bi_valid P) P | 0.
 Proof. by rewrite /AsValid. Qed.
 Global Instance as_valid_entails {PROP : bi} (P Q : PROP) : AsValid0 (P ⊢ Q) (P -∗ Q).
@@ -1031,6 +1032,14 @@ Proof. split. apply bi.entails_wand. apply bi.wand_entails. Qed.
 Global Instance as_valid_equiv {PROP : bi} (P Q : PROP) : AsValid0 (P ≡ Q) (P ∗-∗ Q).
 Proof. split. apply bi.equiv_wand_iff. apply bi.wand_iff_equiv. Qed.
 
+Global Instance as_valid_forall {A : Type} (φ : A → Prop) (P : A → PROP) :
+  (∀ x, AsValid (φ x) (P x)) → AsValid (∀ x, φ x) (∀ x, P x).
+Proof.
+  rewrite /AsValid=>H1. split=>H2.
+  - apply bi.forall_intro=>?. apply H1, H2.
+  - intros x. apply H1. revert H2. by rewrite (bi.forall_elim x).
+Qed.
+
 Global Instance as_valid_embed `{BiEmbedding PROP PROP'} (φ : Prop) (P : PROP) :
   AsValid0 φ P → AsValid φ ⎡P⎤.
 Proof. rewrite /AsValid0 /AsValid=> ->. rewrite bi_embed_valid //. Qed.

theories/tests/proofmode_monpred.v

@@ -55,4 +55,13 @@ Section tests.
   Proof.
     iIntros. by iApply monPred_in_elim.
   Qed.
+
+  Lemma test_iStartProof_forall_1 (Φ : nat → monPredI) : ∀ n, Φ n -∗ Φ n.
+  Proof.
+    iStartProof PROP. iIntros (n i) "$".
+  Qed.
+  Lemma test_iStartProof_forall_2 (Φ : nat → monPredI) : ∀ n, Φ n -∗ Φ n.
+  Proof.
+    iStartProof. iIntros (n) "$".
+  Qed.
 End tests.