diff --git a/algebra/upred_tactics.v b/algebra/upred_tactics.v
index 07e20d9a26f1bc7da8dbbcefe820223b29b32cd2..9605b0c36aeae163b43c9b0dc56669f543cbbfb3 100644
--- a/algebra/upred_tactics.v
+++ b/algebra/upred_tactics.v
@@ -127,3 +127,16 @@ Tactic Notation "cancel" constr(Ps) :=
         [cbv; reflexivity|cbv; reflexivity|simpl]
      end
   end.
+
+Tactic Notation "ecancel" open_constr(Ps) :=
+  let rec close Ps Qs tac :=
+    lazymatch Ps with
+    | [] => tac Qs
+    | ?P :: ?Ps =>
+      find_pat P ltac:(fun Q => close Ps (Q :: Qs) tac)
+    end
+  in
+    lazymatch goal with
+    | |- @uPred_entails ?M _ _ =>
+       close Ps (@nil (uPred M)) ltac:(fun Qs => cancel Qs)
+    end. 
diff --git a/heap_lang/heap.v b/heap_lang/heap.v
index 35889809ffb6e2dadd7bc4db1d01f27ef5543eba..46b8679129cb0476b4bcf748fcad6bf2f0ea8a54 100644
--- a/heap_lang/heap.v
+++ b/heap_lang/heap.v
@@ -131,7 +131,7 @@ Section heap.
     rewrite -(exist_intro (op {[ l := Excl v ]})).
     repeat erewrite <-exist_intro by apply _; simpl.
     rewrite -of_heap_insert left_id right_id.
-    cancel [auth_own heap_name {[l := Excl v]} -★ Φ (LocV l)]%I.
+    ecancel [_ -★ Φ _]%I.
     rewrite -(map_insert_singleton_op h); last by apply of_heap_None.
     rewrite const_equiv ?left_id; last by apply (map_insert_valid h).
     apply later_intro.
diff --git a/prelude/tactics.v b/prelude/tactics.v
index f8cdd865f8a325b63f260cf1fc23afb11bd2e358..5ca37ea3770b482ade80923ddbdf59349d9c6182 100644
--- a/prelude/tactics.v
+++ b/prelude/tactics.v
@@ -298,6 +298,14 @@ Tactic Notation "feed" "destruct" constr(H) :=
 Tactic Notation "feed" "destruct" constr(H) "as" simple_intropattern(IP) :=
   feed (fun p => let H':=fresh in pose proof p as H'; destruct H' as IP) H.
 
+
+(** The following tactic can be used to add support for patterns to tactic notation:
+It will search for the first subterm of the goal matching [pat], and then call [tac]
+with that subterm. *)
+Ltac find_pat pat tac :=
+  match goal with |- context [?x] => unify pat x; tac x || fail 2
+end.
+
 (** Coq's [firstorder] tactic fails or loops on rather small goals already. In 
 particular, on those generated by the tactic [unfold_elem_ofs] which is used
 to solve propositions on collections. The [naive_solver] tactic implements an
diff --git a/program_logic/auth.v b/program_logic/auth.v
index 43342d9be96d932564f50a0f0e5bc60d1a4425d2..9e4634b932ce8c7494a14e9dd06a06585e511cf0 100644
--- a/program_logic/auth.v
+++ b/program_logic/auth.v
@@ -56,7 +56,7 @@ Section auth.
     rewrite sep_exist_l. apply exist_elim=>γ. rewrite -(exist_intro γ).
     trans (▷ auth_inv γ φ ★ auth_own γ a)%I.
     { rewrite /auth_inv -(exist_intro a) later_sep.
-      rewrite const_equiv // left_id. cancel [▷ φ a]%I.
+      rewrite const_equiv // left_id. ecancel [▷ φ _]%I.
       by rewrite -later_intro /auth_own -own_op auth_both_op. }
     rewrite (inv_alloc N) /auth_ctx pvs_frame_r. apply pvs_mono.
     by rewrite always_and_sep_l.
diff --git a/program_logic/sts.v b/program_logic/sts.v
index 7121c370bb1d8d920aa809e0a1b6f1342900f211..4721bb40ad4647d200ae23d9e84862258b1197c3 100644
--- a/program_logic/sts.v
+++ b/program_logic/sts.v
@@ -85,7 +85,7 @@ Section sts.
     rewrite sep_exist_l. apply exist_elim=>γ. rewrite -(exist_intro γ).
     trans (▷ sts_inv γ φ ★ sts_own γ s (⊤ ∖ sts.tok s))%I.
     { rewrite /sts_inv -(exist_intro s) later_sep.
-      cancel [▷ φ s]%I.
+      ecancel [▷ φ _]%I.
       by rewrite -later_intro -own_op sts_op_auth_frag_up; last set_solver. }
     rewrite (inv_alloc N) /sts_ctx pvs_frame_r.
     by rewrite always_and_sep_l.
@@ -114,7 +114,7 @@ Section sts.
   Proof.
     intros Hstep. rewrite /sts_inv /sts_own -(exist_intro s') later_sep.
     (* TODO it would be really nice to use cancel here *)
-    rewrite [(_ ★ ▷φ _)%I]comm -assoc.
+    rewrite [(_ ★ ▷ φ _)%I]comm -assoc.
     rewrite -pvs_frame_l. apply sep_mono_r. rewrite -later_intro.
     rewrite own_valid_l discrete_validI. apply const_elim_sep_l=>Hval.
     trans (|={E}=> own γ (sts_auth s' T'))%I.