diff --git a/theories/proofmode/monpred.v b/theories/proofmode/monpred.v
index 10948e7ce6b81e43a4af41dc64d282ac550d90e9..8b2c7657d4a0068f88daf2e5d58e4dc4ddcceebb 100644
--- a/theories/proofmode/monpred.v
+++ b/theories/proofmode/monpred.v
@@ -267,6 +267,17 @@ Proof.
   rewrite /IntoForall /MakeMonPredAt=>H. setoid_rewrite <- H. by unseal.
 Qed.
 
+Global Instance from_exist_monPred_at_ex P (Φ : I → PROP) i :
+  (∀ i, MakeMonPredAt i P (Φ i)) → FromExist (monPred_ex P i) Φ.
+Proof.
+  rewrite /FromExist /MakeMonPredAt=>H. setoid_rewrite <- H. by unseal.
+Qed.
+Global Instance into_exist_monPred_at_ex P (Φ : I → PROP) i :
+  (∀ i, MakeMonPredAt i P (Φ i)) → IntoExist (monPred_ex P i) Φ.
+Proof.
+  rewrite /IntoExist /MakeMonPredAt=>H. setoid_rewrite <- H. by unseal.
+Qed.
+
 Global Instance from_forall_monPred_at {A} P (Φ : A → monPred) (Ψ : A → PROP) i :
   FromForall P Φ → (∀ a, MakeMonPredAt i (Φ a) (Ψ a)) → FromForall (P i) Ψ.
 Proof.