diff --git a/algebra/sts.v b/algebra/sts.v
index b1683837b021c9ffb0ece93683f235e63babae16..701a5684b10023934ca36f42aa45ba80252e0b93 100644
--- a/algebra/sts.v
+++ b/algebra/sts.v
@@ -240,26 +240,15 @@ Proof.
   - by destruct 1; simpl; intros ?; setoid_subst.
   - by intros ? [|]; destruct 1; inversion_clear 1; constructor; setoid_subst.
   - by do 2 destruct 1; constructor; setoid_subst.
-  - (* (* assert (∀ T T' S s,
-      closed S T → s ∈ S → tok s ∩ T' ≡ ∅ → tok s ∩ (T ∪ T') ≡ ∅).
-    { intros S T T' s [??]. set_solver. } *)
-
-
-    destruct 3; simpl in *; destruct_conjs;
-      repeat match goal with H : closed _ _ |- _ => destruct H end; eauto using closed_op with sts.
-split. auto with sts. 
-
- destruct_conjs. eauto using closed_op with sts.
-admit.
-eapply H. eauto. eauto. *) admit.
+  - destruct 3; simpl in *; destruct_conjs; eauto using closed_op;
+      match goal with H : closed _ _ |- _ => destruct H end; set_solver.
   - intros []; simpl; intros; destruct_conjs; split;
       eauto using closed_up, up_non_empty, closed_up_set, up_set_empty with sts.
   - intros ???? (z&Hy&?&Hxz); destruct Hxz; inversion Hy; clear Hy;
       setoid_subst; destruct_conjs; split_and?;
       rewrite disjoint_union_difference //;
       eauto using up_set_non_empty, up_non_empty, closed_up, closed_disjoint; [].
-    eapply closed_up_set. intros.
-    eapply closed_disjoint; eauto with sts.
+    eapply closed_up_set=> s ?; eapply closed_disjoint; eauto with sts.
   - intros [] [] []; constructor; rewrite ?assoc; auto with sts.
   - destruct 4; inversion_clear 1; constructor; auto with sts.
   - destruct 4; inversion_clear 1; constructor; auto with sts.
@@ -396,8 +385,8 @@ Qed.
 Lemma sts_update_auth s1 s2 T1 T2 :
   steps (s1,T1) (s2,T2) → sts_auth s1 T1 ~~> sts_auth s2 T2.
 Proof.
-  intros ?; apply validity_update; inversion 3 as [|? S ? Tf|]; subst.
-  simpl in *. destruct_conjs.
+  intros ?; apply validity_update.
+  inversion 3 as [|? S ? Tf|]; simplify_eq/=; destruct_conjs.
   destruct (steps_closed s1 s2 T1 T2 S Tf) as (?&?&?); auto; [].
   repeat (done || constructor).
 Qed.
diff --git a/prelude/collections.v b/prelude/collections.v
index a9ff1646571f1a1c6e1154ee93d9cc14d1d07aa2..ff00fcc9b80244c83dffb3941935f2aca5f7d8ad 100644
--- a/prelude/collections.v
+++ b/prelude/collections.v
@@ -262,7 +262,7 @@ Tactic Notation "set_solver" "-" hyp_list(Hs) "/" tactic3(tac) :=
   clear Hs; set_solver tac.
 Tactic Notation "set_solver" "+" hyp_list(Hs) "/" tactic3(tac) :=
   revert Hs; clear; set_solver tac.
-Tactic Notation "set_solver" := set_solver eauto.
+Tactic Notation "set_solver" := set_solver idtac.
 Tactic Notation "set_solver" "-" hyp_list(Hs) := clear Hs; set_solver.
 Tactic Notation "set_solver" "+" hyp_list(Hs) :=
   revert Hs; clear; set_solver.
@@ -537,10 +537,10 @@ Section collection_monad.
 
   Global Instance collection_fmap_mono {A B} :
     Proper (pointwise_relation _ (=) ==> (⊆) ==> (⊆)) (@fmap M _ A B).
-  Proof. intros f g ? X Y ?; set_solver. Qed.
+  Proof. intros f g ? X Y ?; set_solver eauto. Qed.
   Global Instance collection_fmap_proper {A B} :
     Proper (pointwise_relation _ (=) ==> (≡) ==> (≡)) (@fmap M _ A B).
-  Proof. intros f g ? X Y [??]; split; set_solver. Qed.
+  Proof. intros f g ? X Y [??]; split; set_solver eauto. Qed.
   Global Instance collection_bind_mono {A B} :
     Proper (((=) ==> (⊆)) ==> (⊆) ==> (⊆)) (@mbind M _ A B).
   Proof. unfold respectful; intros f g Hfg X Y ?; set_solver. Qed.
@@ -575,12 +575,12 @@ Section collection_monad.
     l ∈ mapM f k ↔ Forall2 (λ x y, x ∈ f y) l k.
   Proof.
     split.
-    - revert l. induction k; set_solver.
+    - revert l. induction k; set_solver eauto.
     - induction 1; set_solver.
   Qed.
   Lemma collection_mapM_length {A B} (f : A → M B) l k :
     l ∈ mapM f k → length l = length k.
-  Proof. revert l; induction k; set_solver. Qed.
+  Proof. revert l; induction k; set_solver eauto. Qed.
   Lemma elem_of_mapM_fmap {A B} (f : A → B) (g : B → M A) l k :
     Forall (λ x, ∀ y, y ∈ g x → f y = x) l → k ∈ mapM g l → fmap f k = l.
   Proof.
diff --git a/program_logic/wsat.v b/program_logic/wsat.v
index 2e9da973fa7fa0b58637fb8ad546c074c0ebfcce..740e56ebb9303ee670516795f3e1ff49f3c398d5 100644
--- a/program_logic/wsat.v
+++ b/program_logic/wsat.v
@@ -102,7 +102,7 @@ Proof.
   { by rewrite (comm _ rP) -assoc big_opM_insert. }
   exists (<[i:=rP]>rs); constructor; rewrite ?Hr; auto.
   - intros j; rewrite Hr lookup_insert_is_Some=>-[?|[??]]; subst.
-    + rewrite !lookup_op HiP !op_is_Some; set_solver +.
+    + split. set_solver. rewrite !lookup_op HiP !op_is_Some; eauto.
     + destruct (HE j) as [Hj Hj']; auto; set_solver +Hj Hj'.
   - intros j P'; rewrite Hr elem_of_union elem_of_singleton=>-[?|?]; subst.
     + rewrite !lookup_wld_op_l ?HiP; auto=> HP.
@@ -162,7 +162,8 @@ Proof.
     + by rewrite lookup_op lookup_singleton_ne // left_id.
   - by rewrite -assoc Hr /= left_id.
   - intros j; rewrite -assoc Hr; destruct (decide (j = i)) as [->|].
-    + rewrite /= !lookup_op lookup_singleton !op_is_Some; set_solver +Hi.
+    + intros _; split; first set_solver +Hi.
+      rewrite /= !lookup_op lookup_singleton !op_is_Some; eauto.
     + rewrite lookup_insert_ne //.
       rewrite lookup_op lookup_singleton_ne // left_id; eauto.
   - intros j P'; rewrite -assoc Hr; destruct (decide (j=i)) as [->|].