diff --git a/iris_unsafe.v b/iris_unsafe.v
index 44a55eda56232b87bb603e59a1f84e918d2eb8c8..d8a4251651e036980e37b3ddb0842127717c1fa6 100644
--- a/iris_unsafe.v
+++ b/iris_unsafe.v
@@ -61,11 +61,6 @@ Module Unsafety (RL : RA_T) (C : CORE_LANG).
     by exfalso; omega.
   Qed.
 
-  (* Leibniz equality arise from SSR's case tactic.
-     RJ: I could use this ;-) move to CSetoid? *) (* PDS: Feel free. I'd like to eventually get everything but the robust safety theorem out of this file. *)
-  Lemma equivP {T : Type} `{eqT : Setoid T} {a b : T} : a = b -> a == b.
-  Proof. by move=>->; reflexivity. Qed.
-
   (*
 	Simple monotonicity tactics for props and wsat.
 
@@ -213,7 +208,7 @@ Module Unsafety (RL : RA_T) (C : CORE_LANG).
         exists w'' α; split; [done| split]; last first.
         + by move: HW; rewrite 2! mask_full_union => HW; wsatM HW.
         apply: (IH _ HLt _ _ _ _ HSwâ‚€); last done.
-        rewrite fillE; exists r' rK; split; [exact: equivP | split; [by propsM Hei' |] ].
+        rewrite fillE; exists r' rK; split; [exact: equivR | split; [by propsM Hei' |] ].
         have {HSw} HSw: w ⊑ w'' by transitivity w'.
         by propsM HK.
 
@@ -246,7 +241,7 @@ Module Unsafety (RL : RA_T) (C : CORE_LANG).
       rewrite/= in Hei'; rewrite fill_empty -Hk' in Hei' * => {Hk'}.
       have {HSw₀} HSw₀ : w₀ ⊑ w''' by transitivity w''; first by transitivity w'.
       apply: (IH _ HLt _ _ _ _ HSwâ‚€); last done.
-      rewrite fillE; exists rei' rK; split; [exact: equivP | split; [done |] ].
+      rewrite fillE; exists rei' rK; split; [exact: equivR | split; [done |] ].
       have {HSw HSw' HSw''} HSw: w ⊑ w''' by transitivity w''; first by transitivity w'.
       by propsM HK.
     Qed.
diff --git a/iris_vs.v b/iris_vs.v
index 4f689abc0dd951d4c1a12e39ddef9c77c75e2c32..8f1003bf0103e956d7b183248be9cd26cd58d9ec 100644
--- a/iris_vs.v
+++ b/iris_vs.v
@@ -107,7 +107,7 @@ Module IrisVS (RL : RA_T) (C : CORE_LANG).
       do 8 red in HInv.
       destruct HE as [rs [HE HM] ].
       destruct (rs i) as [ri |] eqn: HLr.
-      - rewrite ->comp_map_remove with (i := i) (r := ri) in HE by (rewrite HLr; reflexivity).
+      - rewrite ->comp_map_remove with (i := i) (r := ri) in HE by now eapply equivR.
         rewrite ->assoc, <- (assoc (_ r)), (comm rf), assoc in HE.
         exists w'.
         exists↓ (ra_proj r · ra_proj ri). { destruct HE as [HE _]. eapply ra_op_valid, ra_op_valid; eauto with typeclass_instances. }
@@ -149,15 +149,15 @@ Module IrisVS (RL : RA_T) (C : CORE_LANG).
       { destruct (rs i) as [rsi |] eqn: EQrsi; subst;
         [| simpl; rewrite ->ra_op_unit by apply _; now apply ra_pos_valid].
         clear - HE EQrsi. destruct HE as [HE _].
-        rewrite ->comp_map_remove with (i:=i) in HE by (erewrite EQrsi; reflexivity).
+        rewrite ->comp_map_remove with (i:=i) in HE by (eapply equivR; eassumption).
         rewrite ->(assoc (_ r)), (comm (_ r)), comm, assoc, <-(assoc (_ rsi) _), (comm _ (ra_proj r)), assoc in HE.
         eapply ra_op_valid, ra_op_valid; now eauto with typeclass_instances.
       }
       exists (fdUpdate i rri rs); split; [| intros j Hm].
       - simpl. erewrite ra_op_unit by apply _.
         clear - HE EQri. destruct (rs i) as [rsi |] eqn: EQrsi.
-        + subst rsi. erewrite <-comp_map_insert_old; [ eassumption | rewrite EQrsi; reflexivity | reflexivity ].
-        + unfold rri. subst ri. simpl. erewrite <-comp_map_insert_new; [|rewrite EQrsi; reflexivity]. simpl.
+        + subst rsi. erewrite <-comp_map_insert_old; [ eassumption | eapply equivR; eassumption | reflexivity ].
+        + unfold rri. subst ri. simpl. erewrite <-comp_map_insert_new; [|now eapply equivR]. simpl.
           erewrite ra_op_unit by apply _. assumption.
       - specialize (HD j); unfold mask_sing, mask_set, mcup in *; simpl in Hm, HD.
         destruct (Peano_dec.eq_nat_dec i j);
@@ -321,7 +321,7 @@ Module IrisVS (RL : RA_T) (C : CORE_LANG).
         }
         split.
         {
-          rewrite <-comp_map_insert_new by (rewrite HRi; reflexivity).
+          rewrite <-comp_map_insert_new by now eapply equivR.
           rewrite ->assoc, (comm rf). assumption.
         }
         intros j Hm'.
diff --git a/lib/ModuRes/CSetoid.v b/lib/ModuRes/CSetoid.v
index 223a7089e4ebbe130a164b06fce19e1755a076cb..99b90253ea38646e00bb12d9454e0ea603c8833c 100644
--- a/lib/ModuRes/CSetoid.v
+++ b/lib/ModuRes/CSetoid.v
@@ -16,6 +16,13 @@ Generalizable Variables T U V W.
 Definition equiv `{Setoid T} := SetoidClass.equiv.
 Arguments equiv {_ _} _ _ /.
 
+(* Proof by reflexivity *)
+Lemma equivR {T : Type} `{eqT : Setoid T} {a b : T} :
+  a = b -> a == b.
+Proof.
+  intros Heq. subst a. reflexivity.
+Qed.
+
 Notation "'mkType' R" := (@Build_Setoid _ R _) (at level 10).
 
 (** A morphism between two types is an actual function together with a