diff --git a/iris_meta.v b/iris_meta.v
index ea4bf5dd7825632393c9bf2182278203461f8dd4..1e7d09779cbadfce5acfa2c0cc9753bed6bdf469 100644
--- a/iris_meta.v
+++ b/iris_meta.v
@@ -155,7 +155,7 @@ Module IrisMeta (RL : RA_T) (C : CORE_LANG).
     Next Obligation.
       intros x y H_xy P m r. simpl in H_xy. destruct n.
       - intros LEZ. exfalso. omega.
-      - intros _. simpl. assert(H_xy': equiv x y) by assumption. rewrite H_xy'. tauto.
+      - intros _. simpl. assert(H_xy': x == y) by assumption. rewrite H_xy'. tauto.
     Qed.
 
       
@@ -217,7 +217,7 @@ Module IrisMeta (RL : RA_T) (C : CORE_LANG).
     Next Obligation.
       intros x y H_xy P m r. simpl in H_xy. destruct n.
       - intros LEZ. exfalso. omega.
-      - intros _. simpl. assert(H_xy': equiv x y) by assumption. rewrite H_xy'. tauto.
+      - intros _. simpl. assert(H_xy': x == y) by assumption. rewrite H_xy'. tauto.
     Qed.
 
     Program Definition plugExpr safe m φ P Q: expr -n> Props :=
diff --git a/iris_vs.v b/iris_vs.v
index 28698618fcfa49591f6a994e5b6b3676cc8f5523..e2aa64da722e40335778f237c4ac9f5eb4117a60 100644
--- a/iris_vs.v
+++ b/iris_vs.v
@@ -168,7 +168,7 @@ Module IrisVS (RL : RA_T) (C : CORE_LANG).
         rewrite ->HSub in HP; specialize (HSub i); rewrite HLu in HSub.
         destruct (w' i) as [Ï€' |]; [| contradiction].
         split; [intuition now eauto | intros].
-        simpl in HLw, HSub. change (equiv rri ri0) in HLrs. rewrite <- HLw, <- HSub.
+        simpl in HLw, HSub. change (rri == ri0) in HLrs. rewrite <- HLw, <- HSub.
         apply HInv; [now auto with arith |].
         eapply uni_pred, HP; [now auto with arith |].
         rewrite <-HLrs. clear dependent ri0.
diff --git a/lib/ModuRes/RA.v b/lib/ModuRes/RA.v
index 2e2997354aecaecac70bf7589b4916699bffcaef..9c4e14498ee36499dfacc15d476ea07d743d6213 100644
--- a/lib/ModuRes/RA.v
+++ b/lib/ModuRes/RA.v
@@ -271,16 +271,13 @@ Section Exclusive.
       | _, _ => False
     end.
 
-  Global Program Instance ra_eq_equiv : Equivalence ra_res_ex_eq.
-  Next Obligation.
-    intros [t| |]; simpl; now auto.
-  Qed.
-  Next Obligation.
-    intros [t1| |] [t2| |]; simpl; now auto.
-  Qed.
-  Next Obligation.
-    intros [t1| |] [t2| |] [t3| |]; simpl; try now auto.
-    - intros ? ?. etransitivity; eassumption.
+  Global Instance ra_eq_equiv : Equivalence ra_res_ex_eq.
+  Proof.
+    split.
+    - intros [t| |]; simpl; now auto.
+    - intros [t1| |] [t2| |]; simpl; now auto.
+    - intros [t1| |] [t2| |] [t3| |]; simpl; try now auto.
+      + intros ? ?. etransitivity; eassumption.
   Qed.
 
   Global Program Instance ra_type_ex : Setoid ra_res_ex :=
diff --git a/masks.v b/masks.v
index c20ae8ae45a9b10a2ba4762b77bce1937f17ccd5..4fc39102f6bc9274a0639692e9c4f74e8b8c1927 100644
--- a/masks.v
+++ b/masks.v
@@ -1,4 +1,5 @@
 Require Import Arith Program RelationClasses Morphisms.
+Require Import ModuRes.CSetoid.
 
 Definition mask := nat -> Prop.
 
@@ -28,8 +29,16 @@ Definition mcup (m1 m2 : mask) : mask :=
 Definition mminus (m1 m2 : mask) : mask :=
   fun i => (m1 : mask) i /\ ~ (m2 : mask) i.
 
+Global Instance meq_Equivalence: Equivalence meq.
+Proof.
+  split.
+  - intros m. unfold meq. tauto.
+  - intros m1 m2. unfold meq. now auto.
+  - intros m1 m2 m3. unfold meq. now firstorder.
+Qed.
+Global Instance mask_type : Setoid mask := mkType meq.
+
 Delimit Scope mask_scope with mask.
-Notation "m1 == m2" := (meq m1 m2) (at level 70) : mask_scope.
 Notation "m1 ⊆ m2"  := (mle m1 m2)  (at level 70) : mask_scope.
 Notation "m1 ∩ m2" := (mcap m1 m2) (at level 40) : mask_scope.
 Notation "m1 \  m2"  := (mminus m1 m2) (at level 30) : mask_scope.