diff --git a/theories/proofmode/class_instances.v b/theories/proofmode/class_instances.v
index 7694c59b644f63a2fd7b9ce404600113c3e2fc78..2fd3fa1ca8ceabc3f4dc6ff1486e39afedc3219e 100644
--- a/theories/proofmode/class_instances.v
+++ b/theories/proofmode/class_instances.v
@@ -55,6 +55,15 @@ Global Instance into_pure_forall {X : Type} (Î¦ : X â†’ uPred M) Ï† :
 Proof.
   rewrite /IntoPure=>Hx. rewrite -pure_forall_2. by setoid_rewrite Hx.
 Qed.
+Global Instance into_pure_pure_conj (Ï†1 Ï†2 : uPred M) P1 P2 :
+  IntoPure Ï†1 P1 -> IntoPure Ï†2 P2 -> IntoPure (Ï†1 âˆ§ Ï†2) (P1 âˆ§ P2).
+Proof. rewrite /IntoPure pure_and. by intros -> ->. Qed.
+Global Instance into_pure_pure_sep (Ï†1 Ï†2 : uPred M) P1 P2 :
+  IntoPure Ï†1 P1 -> IntoPure Ï†2 P2 -> IntoPure (Ï†1 âˆ— Ï†2) (P1 âˆ§ P2).
+Proof. rewrite /IntoPure sep_and pure_and. by intros -> ->. Qed.
+Global Instance into_pure_pure_disj (Ï†1 Ï†2 : uPred M) P1 P2 :
+  IntoPure Ï†1 P1 -> IntoPure Ï†2 P2 -> IntoPure (Ï†1 âˆ¨ Ï†2) (P1 âˆ¨ P2).
+Proof. rewrite /IntoPure pure_or. by intros -> ->. Qed.
 
 (* FromPure *)
 Global Instance from_pure_pure Ï† : @FromPure M âŒœÏ†âŒ Ï†.