diff --git a/modures/logic.v b/modures/logic.v
index 64ffb9f7fb519d1d21701f977638b41810cf416c..1b377b7222a4bdb2ab778c31bcb0df2908416b56 100644
--- a/modures/logic.v
+++ b/modures/logic.v
@@ -134,9 +134,9 @@ Next Obligation.
   assert (∃ x2', y ={n2}= x1 ⋅ x2' ∧ x2 ≼ x2') as (x2'&Hy&?).
   { destruct Hxy as [z Hy]; exists (x2 â‹… z); split; eauto using @ra_included_l.
     apply dist_le with n1; auto. by rewrite (associative op) -Hx Hy. }
-  exists x1, x2'; split_ands; [done| |].
-  * cofe_subst y; apply uPred_weaken with x1 n1; eauto using cmra_valid_op_l.
-  * cofe_subst y; apply uPred_weaken with x2 n1; eauto using cmra_valid_op_r.
+  clear Hxy; cofe_subst y; exists x1, x2'; split_ands; [done| |].
+  * apply uPred_weaken with x1 n1; eauto using cmra_valid_op_l.
+  * apply uPred_weaken with x2 n1; eauto using cmra_valid_op_r.
 Qed.
 
 Program Definition uPred_wand {M} (P Q : uPred M) : uPred M :=
diff --git a/prelude/tactics.v b/prelude/tactics.v
index c2190568d733add0f43597a64b05d57d01df5563..85c0fd52a54257bc9ffbad52eb355ea039478895 100644
--- a/prelude/tactics.v
+++ b/prelude/tactics.v
@@ -218,7 +218,7 @@ Ltac setoid_subst_aux R x :=
         try match H' with H => fail 2 end;
         setoid_rewrite H in H'
      end;
-     clear H
+     clear x H
   end.
 Ltac setoid_subst :=
   repeat match goal with