diff --git a/theories/proofmode/class_instances.v b/theories/proofmode/class_instances.v
index db9633a91c9d501b68a550bab15c79b3bea73368..4557f7908d4e1669e2ac714f2a40fd706082ef8c 100644
--- a/theories/proofmode/class_instances.v
+++ b/theories/proofmode/class_instances.v
@@ -43,32 +43,32 @@ Global Instance into_pure_cmra_valid `{CMRADiscrete A} (a : A) :
   @IntoPure M (âœ“ a) (âœ“ a).
 Proof. by rewrite /IntoPure discrete_valid. Qed.
 
-Global Instance into_pure_pure_conj (Ï†1 Ï†2 : uPred M) P1 P2 :
-  IntoPure Ï†1 P1 -> IntoPure Ï†2 P2 -> IntoPure (Ï†1 âˆ§ Ï†2) (P1 âˆ§ P2).
+Global Instance into_pure_pure_conj (Ï†1 Ï†2 : Prop) P1 P2 :
+  IntoPure P1 Ï†1 -> IntoPure P2 Ï†2 -> IntoPure (P1 âˆ§ P2) (Ï†1 âˆ§ Ï†2).
 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).
+Global Instance into_pure_pure_sep (Ï†1 Ï†2 : Prop) P1 P2 :
+  IntoPure P1 Ï†1 -> IntoPure P2 Ï†2 -> IntoPure (P1 âˆ— P2) (Ï†1 âˆ§ Ï†2).
 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).
+Global Instance into_pure_pure_disj (Ï†1 Ï†2 : Prop) P1 P2 :
+  IntoPure P1 Ï†1 -> IntoPure P2 Ï†2 -> IntoPure (P1 âˆ¨ P2) (Ï†1 âˆ¨ Ï†2).
 Proof. rewrite /IntoPure pure_or. by intros -> ->. Qed.
-Global Instance into_pure_pure_impl (Ï†1 Ï†2 : uPred M) P1 P2 :
-  FromPure Ï†1 P1 -> IntoPure Ï†2 P2 -> IntoPure (Ï†1 â†’ Ï†2) (P1 â†’ P2).
+Global Instance into_pure_pure_impl (Ï†1 Ï†2 : Prop) P1 P2 :
+  FromPure P1 Ï†1 -> IntoPure P2 Ï†2 -> IntoPure (P1 â†’ P2) (Ï†1 â†’ Ï†2).
 Proof. rewrite /FromPure /IntoPure pure_impl. by intros -> ->. Qed.
-Global Instance into_pure_pure_wand (Ï†1 Ï†2 : uPred M) P1 P2 :
-  FromPure Ï†1 P1 -> IntoPure Ï†2 P2 -> IntoPure (Ï†1 -âˆ— Ï†2) (P1 â†’ P2).
+Global Instance into_pure_pure_wand (Ï†1 Ï†2 : Prop) P1 P2 :
+  FromPure P1 Ï†1 -> IntoPure P2 Ï†2 -> IntoPure (P1 -âˆ— P2) (Ï†1 â†’ Ï†2).
 Proof.
   rewrite /FromPure /IntoPure pure_impl always_impl_wand. by intros -> ->.
 Qed.
 
-Global Instance into_pure_exist {X : Type} (Î¦ : X â†’ uPred M) Ï† :
+Global Instance into_pure_exist {X : Type} (Î¦ : X â†’ uPred M) (Ï† : X â†’ Prop) :
   (âˆ€ x, @IntoPure M (Î¦ x) (Ï† x)) â†’ @IntoPure M (âˆƒ x, Î¦ x) (âˆƒ x, Ï† x).
 Proof.
   rewrite /IntoPure=>Hx. apply exist_elim=>x. rewrite Hx.
   apply pure_elim'=>HÏ†. apply pure_intro. eauto.
 Qed.
 
-Global Instance into_pure_forall {X : Type} (Î¦ : X â†’ uPred M) Ï† :
+Global Instance into_pure_forall {X : Type} (Î¦ : X â†’ uPred M) (Ï† : X â†’ Prop) :
   (âˆ€ x, @IntoPure M (Î¦ x) (Ï† x)) â†’ @IntoPure M (âˆ€ x, Î¦ x) (âˆ€ x, Ï† x).
 Proof.
   rewrite /IntoPure=>Hx. rewrite -pure_forall_2. by setoid_rewrite Hx.
@@ -91,32 +91,31 @@ Qed.
 Global Instance from_pure_bupd P Ï† : FromPure P Ï† â†’ FromPure (|==> P) Ï†.
 Proof. rewrite /FromPure=> ->. apply bupd_intro. Qed.
 
-
-Global Instance from_pure_pure_conj (Ï†1 Ï†2 : uPred M) P1 P2 :
-  FromPure Ï†1 P1 -> FromPure Ï†2 P2 -> FromPure (Ï†1 âˆ§ Ï†2) (P1 âˆ§ P2).
+Global Instance from_pure_pure_conj (Ï†1 Ï†2 : Prop) P1 P2 :
+  FromPure P1 Ï†1 -> FromPure P2 Ï†2 -> FromPure (P1 âˆ§ P2) (Ï†1 âˆ§ Ï†2).
 Proof. rewrite /FromPure pure_and. by intros -> ->. Qed.
-Global Instance from_pure_pure_sep (Ï†1 Ï†2 : uPred M) P1 P2 :
-  FromPure Ï†1 P1 -> FromPure Ï†2 P2 -> FromPure (Ï†1 âˆ— Ï†2) (P1 âˆ§ P2).
+Global Instance from_pure_pure_sep (Ï†1 Ï†2 : Prop) P1 P2 :
+  FromPure P1 Ï†1 -> FromPure P2 Ï†2 -> FromPure (P1 âˆ— P2) (Ï†1 âˆ§ Ï†2).
 Proof. rewrite /FromPure pure_and always_and_sep_l. by intros -> ->. Qed.
-Global Instance from_pure_pure_disj (Ï†1 Ï†2 : uPred M) P1 P2 :
-  FromPure Ï†1 P1 -> FromPure Ï†2 P2 -> FromPure (Ï†1 âˆ¨ Ï†2) (P1 âˆ¨ P2).
+Global Instance from_pure_pure_disj (Ï†1 Ï†2 : Prop) P1 P2 :
+  FromPure P1 Ï†1 -> FromPure P2 Ï†2 -> FromPure (P1 âˆ¨ P2) (Ï†1 âˆ¨ Ï†2).
 Proof. rewrite /FromPure pure_or. by intros -> ->. Qed.
-Global Instance from_pure_pure_impl (Ï†1 Ï†2 : uPred M) P1 P2 :
-  IntoPure Ï†1 P1 -> FromPure Ï†2 P2 -> FromPure (Ï†1 â†’ Ï†2) (P1 â†’ P2).
+Global Instance from_pure_pure_impl (Ï†1 Ï†2 : Prop) P1 P2 :
+  IntoPure P1 Ï†1 -> FromPure P2 Ï†2 -> FromPure (P1 â†’ P2) (Ï†1 â†’ Ï†2).
 Proof. rewrite /FromPure /IntoPure pure_impl. by intros -> ->. Qed.
-Global Instance from_pure_pure_wand (Ï†1 Ï†2 : uPred M) P1 P2 :
-  IntoPure Ï†1 P1 -> FromPure Ï†2 P2 -> FromPure (Ï†1 -âˆ— Ï†2) (P1 â†’ P2).
+Global Instance from_pure_pure_wand (Ï†1 Ï†2 : Prop) P1 P2 :
+  IntoPure P1 Ï†1 -> FromPure P2 Ï†2 -> FromPure (P1 -âˆ— P2) (Ï†1 â†’ Ï†2).
 Proof.
   rewrite /FromPure /IntoPure pure_impl always_impl_wand. by intros -> ->.
 Qed.
 
-Global Instance from_pure_exist {X : Type} (Î¦ : X â†’ uPred M) Ï† :
+Global Instance from_pure_exist {X : Type} (Î¦ : X â†’ uPred M) (Ï† : X â†’ Prop) :
   (âˆ€ x, @FromPure M (Î¦ x) (Ï† x)) â†’ @FromPure M (âˆƒ x, Î¦ x) (âˆƒ x, Ï† x).
 Proof.
   rewrite /FromPure=>Hx. apply pure_elim'=>-[x ?]. rewrite -(exist_intro x).
   rewrite -Hx. apply pure_intro. done.
 Qed.
-Global Instance from_pure_forall {X : Type} (Î¦ : X â†’ uPred M) Ï† :
+Global Instance from_pure_forall {X : Type} (Î¦ : X â†’ uPred M) (Ï† : X â†’ Prop) :
   (âˆ€ x, @FromPure M (Î¦ x) (Ï† x)) â†’ @FromPure M (âˆ€ x, Î¦ x) (âˆ€ x, Ï† x).
 Proof.
   rewrite /FromPure=>Hx. apply forall_intro=>x. apply pure_elim'=>HÏ†.