diff --git a/algebra/dra.v b/algebra/dra.v
index 22183991bb352a74d4196a37b33dcec680ec2397..756508e1fa636527f6c58e1fd36ab2a1c3a3b4a2 100644
--- a/algebra/dra.v
+++ b/algebra/dra.v
@@ -142,12 +142,12 @@ Lemma to_validity_valid (x : A) :
   ✓ to_validity x → ✓ x.
 Proof. intros. done. Qed.
 Lemma to_validity_op (x y : A) :
-  ✓ x → ✓ y → (✓ (x ⋅ y) → x ⊥ y) →
+  (✓ (x ⋅ y) → ✓ x ∧ ✓ y ∧ x ⊥ y) →
   to_validity (x ⋅ y) ≡ to_validity x ⋅ to_validity y.
 Proof.
-  intros Hvalx Hvaly Hdisj. split; [split | done].
+  intros Hvd. split; [split | done].
   - simpl. auto.
-  - simpl. intros (_ & _ & ?).
+  - clear Hvd. simpl. intros (? & ? & ?).
     auto using dra_op_valid, to_validity_valid.
 Qed.
 
diff --git a/algebra/sts.v b/algebra/sts.v
index 9a35709b4cbb8fdde6643f0fb111598994634057..29e4b561cf00d53ad4a2d95c7109e86a3f18eea4 100644
--- a/algebra/sts.v
+++ b/algebra/sts.v
@@ -36,8 +36,7 @@ Inductive frame_step (T : tokens sts) (s1 s2 : state sts) : Prop :=
 
 (** ** Closure under frame steps *)
 Record closed (S : states sts) (T : tokens sts) : Prop := Closed {
-  closed_ne : S ≢ ∅;
-  closed_disjoint s : s ∈ S → tok s ∩ T ⊆ ∅;
+  closed_disjoint s : s ∈ S → tok s ∩ T ≡ ∅;
   closed_step s1 s2 : s1 ∈ S → frame_step T s1 s2 → s2 ∈ S
 }.
 Definition up (s : state sts) (T : tokens sts) : states sts :=
@@ -47,10 +46,10 @@ Definition up_set (S : states sts) (T : tokens sts) : states sts :=
 
 (** Tactic setup *)
 Hint Resolve Step.
-Hint Extern 10 (equiv (A:=set _) _ _) => set_solver : sts.
-Hint Extern 10 (¬equiv (A:=set _) _ _) => set_solver : sts.
-Hint Extern 10 (_ ∈ _) => set_solver : sts.
-Hint Extern 10 (_ ⊆ _) => set_solver : sts.
+Hint Extern 50 (equiv (A:=set _) _ _) => set_solver : sts.
+Hint Extern 50 (¬equiv (A:=set _) _ _) => set_solver : sts.
+Hint Extern 50 (_ ∈ _) => set_solver : sts.
+Hint Extern 50 (_ ⊆ _) => set_solver : sts.
 
 (** ** Setoids *)
 Instance framestep_mono : Proper (flip (⊆) ==> (=) ==> (=) ==> impl) frame_step.
@@ -84,16 +83,13 @@ Global Instance up_set_proper : Proper ((≡) ==> (≡) ==> (≡)) up_set.
 Proof. by intros S1 S2 [??] T1 T2 [??]; split; apply up_set_preserving. Qed.
 
 (** ** Properties of closure under frame steps *)
-Lemma closed_disjoint' S T s : closed S T → s ∈ S → tok s ∩ T ≡ ∅.
-Proof. intros [_ ? _]; set_solver. Qed.
 Lemma closed_steps S T s1 s2 :
   closed S T → s1 ∈ S → rtc (frame_step T) s1 s2 → s2 ∈ S.
 Proof. induction 3; eauto using closed_step. Qed.
 Lemma closed_op T1 T2 S1 S2 :
-  closed S1 T1 → closed S2 T2 →
-  T1 ∩ T2 ≡ ∅ → S1 ∩ S2 ≢ ∅ → closed (S1 ∩ S2) (T1 ∪ T2).
+  closed S1 T1 → closed S2 T2 → closed (S1 ∩ S2) (T1 ∪ T2).
 Proof.
-  intros [_ ? Hstep1] [_ ? Hstep2] ?; split; [done|set_solver|].
+  intros [? Hstep1] [? Hstep2]; split; [set_solver|].
   intros s3 s4; rewrite !elem_of_intersection; intros [??] [T3 T4 ?]; split.
   - apply Hstep1 with s3, Frame_step with T3 T4; auto with sts.
   - apply Hstep2 with s3, Frame_step with T3 T4; auto with sts.
@@ -102,7 +98,7 @@ Lemma step_closed s1 s2 T1 T2 S Tf :
   step (s1,T1) (s2,T2) → closed S Tf → s1 ∈ S → T1 ∩ Tf ≡ ∅ →
   s2 ∈ S ∧ T2 ∩ Tf ≡ ∅ ∧ tok s2 ∩ T2 ≡ ∅.
 Proof.
-  inversion_clear 1 as [???? HR Hs1 Hs2]; intros [?? Hstep]??; split_and?; auto.
+  inversion_clear 1 as [???? HR Hs1 Hs2]; intros [? Hstep]??; split_and?; auto.
   - eapply Hstep with s1, Frame_step with T1 T2; auto with sts.
   - set_solver -Hstep Hs1 Hs2.
 Qed.
@@ -125,26 +121,35 @@ Proof. intros s ?; apply elem_of_bind; eauto using elem_of_up. Qed.
 Lemma up_up_set s T : up s T ≡ up_set {[ s ]} T.
 Proof. by rewrite /up_set collection_bind_singleton. Qed.
 Lemma closed_up_set S T :
-  (∀ s, s ∈ S → tok s ∩ T ⊆ ∅) → S ≢ ∅ → closed (up_set S T) T.
+  (∀ s, s ∈ S → tok s ∩ T ≡ ∅) → closed (up_set S T) T.
 Proof.
-  intros HS Hne; unfold up_set; split.
-  - assert (∀ s, s ∈ up s T) by eauto using elem_of_up. set_solver.
+  intros HS; unfold up_set; split.
   - intros s; rewrite !elem_of_bind; intros (s'&Hstep&Hs').
-    specialize (HS s' Hs'); clear Hs' Hne S.
+    specialize (HS s' Hs'); clear Hs' S.
     induction Hstep as [s|s1 s2 s3 [T1 T2 ? Hstep] ? IH]; first done.
     inversion_clear Hstep; apply IH; clear IH; auto with sts.
   - intros s1 s2; rewrite !elem_of_bind; intros (s&?&?) ?; exists s.
     split; [eapply rtc_r|]; eauto.
 Qed.
-Lemma closed_up_set_empty S : S ≢ ∅ → closed (up_set S ∅) ∅.
-Proof. eauto using closed_up_set with sts. Qed.
 Lemma closed_up s T : tok s ∩ T ≡ ∅ → closed (up s T) T.
 Proof.
   intros; rewrite -(collection_bind_singleton (λ s, up s T) s).
   apply closed_up_set; set_solver.
 Qed.
+Lemma closed_up_set_empty S : closed (up_set S ∅) ∅.
+Proof. eauto using closed_up_set with sts. Qed.
 Lemma closed_up_empty s : closed (up s ∅) ∅.
 Proof. eauto using closed_up with sts. Qed.
+Lemma up_set_empty S T : up_set S T ≡ ∅ → S ≡ ∅.
+Proof.
+  move:(subseteq_up_set S T). set_solver.
+Qed.
+Lemma up_set_nonempty S T : S ≢ ∅ → up_set S T ≢ ∅.
+Proof. by move=>? /up_set_empty. Qed.
+Lemma up_nonempty s T : up s T ≢ ∅.
+Proof.
+  move:(elem_of_up s T). set_solver.
+Qed.
 Lemma up_closed S T : closed S T → up_set S T ≡ S.
 Proof.
   intros; split; auto using subseteq_up_set; intros s.
@@ -186,7 +191,9 @@ Inductive sts_equiv : Equiv (car sts) :=
   | frag_equiv S1 S2 T1 T2 : T1 ≡ T2 → S1 ≡ S2 → frag S1 T1 ≡ frag S2 T2.
 Existing Instance sts_equiv.
 Instance sts_valid : Valid (car sts) := λ x,
-  match x with auth s T => tok s ∩ T ≡ ∅ | frag S' T => closed S' T end.
+  match x with
+  | auth s T => tok s ∩ T ≡ ∅
+  | frag S' T => closed S' T ∧ S' ≢ ∅ end.
 Instance sts_unit : Unit (car sts) := λ x,
   match x with
   | frag S' _ => frag (up_set S' ∅ ) ∅
@@ -238,29 +245,36 @@ Proof.
   - 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 *; auto using closed_op with sts.
-  - intros []; simpl; eauto using closed_up, closed_up_set, closed_ne with sts.
-  - intros ???? (z&Hy&?&Hxz); destruct Hxz; inversion Hy;clear Hy; setoid_subst;
-      rewrite ?disjoint_union_difference; auto using closed_up with sts.
-    eapply closed_up_set; eauto 2 using closed_disjoint with sts.
+    destruct 3; simpl in *; destruct_conjs; auto using closed_op with sts.
+  - intros []; simpl; intros; destruct_conjs; split;
+      eauto using closed_up, up_nonempty, closed_up_set, up_set_empty with sts.
+  - intros ???? (z&Hy&?&Hxz); destruct Hxz; inversion Hy; clear Hy;
+      setoid_subst; destruct_conjs; split_and?;
+      (* TODO improve this. *)
+      eauto using up_set_nonempty, up_nonempty;
+      assert ((T1 ∪ T2) ∖ T1 ≡ T2) as -> by set_solver;
+      eauto using closed_up, closed_disjoint; [].
+    eapply closed_up_set. intros.
+    eapply closed_disjoint; first done. set_solver.
   - 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.
   - destruct 1; constructor; auto with sts.
   - destruct 3; constructor; auto with sts.
   - intros [|S T]; constructor; auto using elem_of_up with sts.
-    assert (S ⊆ up_set S ∅ ∧ S ≢ ∅) by eauto using subseteq_up_set, closed_ne.
+    simpl in *. assert (S ⊆ up_set S ∅) by eauto using subseteq_up_set.
     set_solver.
   - intros [|S T]; constructor; auto with sts.
     assert (S ⊆ up_set S ∅); auto using subseteq_up_set with sts.
   - intros [s T|S T]; constructor; auto with sts.
     + rewrite (up_closed (up _ _)); auto using closed_up with sts.
     + rewrite (up_closed (up_set _ _));
-        eauto using closed_up_set, closed_ne with sts.
+        eauto using closed_up_set with sts.
   - intros x y ?? (z&Hy&?&Hxz); exists (unit (x â‹… y)); split_and?.
     + destruct Hxz;inversion_clear Hy;constructor;unfold up_set; set_solver.
-    + destruct Hxz; inversion_clear Hy; simpl;
-        auto using closed_up_set_empty, closed_up_empty with sts.
+    + destruct Hxz; inversion_clear Hy; simpl; split_and?;
+        auto using closed_up_set_empty, closed_up_empty, up_nonempty; [].
+      eapply up_set_nonempty. set_solver.
     + destruct Hxz; inversion_clear Hy; constructor;
         repeat match goal with
         | |- context [ up_set ?S ?T ] =>
@@ -280,7 +294,7 @@ Proof.
       rewrite ?disjoint_union_difference; auto.
     split; [|apply intersection_greatest; auto using subseteq_up_set with sts].
     apply intersection_greatest; [auto with sts|].
-    intros s2; rewrite elem_of_intersection.
+    intros s2; rewrite elem_of_intersection. destruct_conjs.
     unfold up_set; rewrite elem_of_bind; intros (?&s1&?&?&?).
     apply closed_steps with T2 s1; auto with sts.
 Qed.
@@ -328,10 +342,10 @@ Proof. intros T1 T2 HT. by rewrite /sts_frag_up HT. Qed.
 (** Validity *)
 Lemma sts_auth_valid s T : ✓ sts_auth s T ↔ tok s ∩ T ≡ ∅.
 Proof. split. by move=> /(_ 0). by intros ??. Qed.
-Lemma sts_frag_valid S T : ✓ sts_frag S T ↔ closed S T.
+Lemma sts_frag_valid S T : ✓ sts_frag S T ↔ closed S T ∧ S ≢ ∅.
 Proof. split. by move=> /(_ 0). by intros ??. Qed.
 Lemma sts_frag_up_valid s T : tok s ∩ T ≡ ∅ → ✓ sts_frag_up s T.
-Proof. intros; by apply sts_frag_valid, closed_up. Qed.
+Proof. intros. by apply sts_frag_valid; auto using closed_up, up_nonempty. Qed.
 
 Lemma sts_auth_frag_valid_inv s S T1 T2 :
   ✓ (sts_auth s T1 ⋅ sts_frag S T2) → s ∈ S.
@@ -342,32 +356,36 @@ Lemma sts_op_auth_frag s S T :
   s ∈ S → closed S T → sts_auth s ∅ ⋅ sts_frag S T ≡ sts_auth s T.
 Proof.
   intros; split; [split|constructor; set_solver]; simpl.
-  - intros (?&?&?); by apply closed_disjoint' with S.
+  - intros (?&?&?); by apply closed_disjoint with S.
   - intros; split_and?.
     + set_solver+.
     + done.
+    + set_solver.
     + constructor; set_solver.
 Qed.
 Lemma sts_op_auth_frag_up s T :
   sts_auth s ∅ ⋅ sts_frag_up s T ≡ sts_auth s T.
 Proof.
   intros; split; [split|constructor; set_solver]; simpl.
-  - intros (?&?&?). apply closed_disjoint' with (up s T); first done.
+  - intros (?&?&?). destruct_conjs.
+    apply closed_disjoint with (up s T); first done.
     apply elem_of_up.
   - intros; split_and?.
     + set_solver+.
     + by apply closed_up.
+    + apply up_nonempty.
     + constructor; last set_solver. apply elem_of_up.
 Qed.
 
 Lemma sts_op_frag S1 S2 T1 T2 :
-  T1 ∩ T2 ⊆ ∅ → sts.closed S1 T1 → sts.closed S2 T2 →
+  T1 ∩ T2 ≡ ∅ → sts.closed S1 T1 → sts.closed S2 T2 →
   sts_frag (S1 ∩ S2) (T1 ∪ T2) ≡ sts_frag S1 T1 ⋅ sts_frag S2 T2.
 Proof.
   intros HT HS1 HS2. rewrite /sts_frag.
   (* FIXME why does rewrite not work?? *)
-  etrans; last eapply to_validity_op; try done; [].
-  intros Hval. constructor; last set_solver. eapply closed_ne, Hval.
+  etrans; last eapply to_validity_op; first done; [].
+  move=>/=[??]. split_and!; [auto; set_solver..|].
+  constructor; done.
 Qed.
 
 (** Frame preserving updates *)
@@ -375,28 +393,31 @@ 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.
   destruct (steps_closed s1 s2 T1 T2 S Tf) as (?&?&?); auto; [].
   repeat (done || constructor).
 Qed.
 
-Lemma sts_update_frag S1 S2 T :
-  closed S2 T → S1 ⊆ S2 → sts_frag S1 T ~~> sts_frag S2 T.
+Lemma sts_update_frag S1 S2 T1 T2 :
+  closed S2 T2 → S1 ⊆ S2 → T2 ⊆ T1 → sts_frag S1 T1 ~~> sts_frag S2 T2.
 Proof.
-  rewrite /sts_frag=> HS Hcl. apply validity_update.
+  rewrite /sts_frag=> ? HS HT. apply validity_update.
   inversion 3 as [|? S ? Tf|]; simplify_eq/=.
-  - split; first done. constructor; [set_solver|done].
-  - split; first done. constructor; set_solver.
+  - split_and!; first done; first set_solver. constructor; set_solver.
+  - split_and!; first done; first set_solver. constructor; set_solver.
 Qed.
 
-Lemma sts_update_frag_up s1 S2 T :
-  closed S2 T → s1 ∈ S2 → sts_frag_up s1 T ~~> sts_frag S2 T.
+Lemma sts_update_frag_up s1 S2 T1 T2 :
+  closed S2 T2 → s1 ∈ S2 → T2 ⊆ T1 → sts_frag_up s1 T1 ~~> sts_frag S2 T2.
 Proof.
-  intros; by apply sts_update_frag; [|intros ?; eauto using closed_steps].
+  intros ? ? HT; apply sts_update_frag; [intros; eauto using closed_steps..].
+  rewrite <-HT. eapply up_subseteq; done.
 Qed.
 
 (** Inclusion *)
+(*
 Lemma sts_frag_included S1 S2 T1 T2 :
-  closed S2 T2 →
+  closed S2 T2 → S2 ≢ ∅
   sts_frag S1 T1 ≼ sts_frag S2 T2 ↔
   (closed S1 T1 ∧ ∃ Tf, T2 ≡ T1 ∪ Tf ∧ T1 ∩ Tf ≡ ∅ ∧ S2 ≡ S1 ∩ up_set S2 Tf).
 Proof. (* This should use some general properties of DRAs. To be improved
@@ -435,4 +456,5 @@ Proof.
   intros. apply sts_frag_included; split_and?; auto.
   exists ∅; split_and?; done || set_solver+.
 Qed.
+*)
 End stsRA.
diff --git a/barrier/barrier.v b/barrier/barrier.v
index 0c91761e37e2fc58f72c86a863f48bbebca42428..54e758eef18bc8477d086123eb198c30440a8f9b 100644
--- a/barrier/barrier.v
+++ b/barrier/barrier.v
@@ -41,22 +41,18 @@ Module barrier_proto.
     sts.closed (i_states i) {[ Change i ]}.
   Proof.
     split.
-    - apply (non_empty_inhabited(State Low {[ i ]})). rewrite !mkSet_elem_of /=.
-      apply lookup_singleton.
     - move=>[p I]. rewrite /= /tok !mkSet_elem_of /= =>HI.
-      move=>s' /elem_of_intersection. rewrite !mkSet_elem_of /=.
-      move=>[[Htok|Htok] ? ]; subst s'; first done.
-      destruct p; done.
+      destruct p; set_solver.
     - (* If we do the destruct of the states early, and then inversion
          on the proof of a transition, it doesn't work - we do not obtain
          the equalities we need. So we destruct the states late, because this
          means we can use "destruct" instead of "inversion". *)
       move=>s1 s2. rewrite !mkSet_elem_of /==> Hs1 Hstep.
-      (* We probably want some helper lemmas for this... *)
       inversion_clear Hstep as [T1 T2 Hdisj Hstep'].
       inversion_clear Hstep' as [? ? ? ? Htrans _ _ Htok].
       destruct Htrans; last done; move:Hs1 Hdisj Htok.
-      rewrite /= /tok /=.
+      rewrite /= /tok /=. 
+      (* TODO: Can this be done better? *)
       intros. apply dec_stable. 
       assert (Change i ∉ change_tokens I1) as HI1
         by (rewrite mkSet_not_elem_of; set_solver +Hs1).
@@ -74,9 +70,8 @@ Module barrier_proto.
   Lemma low_states_closed : sts.closed low_states {[ Send ]}.
   Proof.
     split.
-    - apply (non_empty_inhabited(State Low ∅)). by rewrite !mkSet_elem_of /=.
     - move=>[p I]. rewrite /= /tok !mkSet_elem_of /= =>HI.
-      destruct p; last done. set_solver.
+      destruct p; set_solver.
     - move=>s1 s2. rewrite !mkSet_elem_of /==> Hs1 Hstep.
       inversion_clear Hstep as [T1 T2 Hdisj Hstep'].
       inversion_clear Hstep' as [? ? ? ? Htrans _ _ Htok].
@@ -101,9 +96,9 @@ Module barrier_proto.
     (* TODO this proof is rather annoying. *)
     apply elem_of_equiv=>t. rewrite !elem_of_union.
     rewrite !mkSet_elem_of /change_tokens /=.
-    destruct t as [j|]; last naive_solver.
+    destruct t as [j|]; last set_solver.
     rewrite elem_of_difference elem_of_singleton.
-    destruct (decide (i = j)); naive_solver.
+    destruct (decide (i = j)); set_solver.
   Qed.
     
   Lemma split_step p i i1 i2 I :
@@ -115,15 +110,12 @@ Module barrier_proto.
     constructor; first constructor; rewrite /= /tok /=; first (destruct p; set_solver).
     (* This gets annoying... and I think I can see a pattern with all these proofs. Automatable? *)
     - apply elem_of_equiv=>t. destruct t; last set_solver.
-      rewrite !mkSet_elem_of /change_tokens /=.
-      rewrite !elem_of_union !elem_of_difference !elem_of_singleton.
-      destruct p; naive_solver.
+      rewrite !mkSet_elem_of. destruct p; set_solver.
     - apply elem_of_equiv=>t. destruct t as [j|]; last set_solver.
-      rewrite !mkSet_elem_of /change_tokens /=.
-      rewrite !elem_of_union !elem_of_difference !elem_of_singleton.
-      destruct (decide (i1 = j)); first naive_solver. 
-      destruct (decide (i2 = j)); first naive_solver.
-      destruct (decide (i = j)); naive_solver.
+      rewrite !mkSet_elem_of.
+      destruct (decide (i1 = j)); first set_solver. 
+      destruct (decide (i2 = j)); first set_solver.
+      destruct (decide (i = j)); set_solver.
   Qed.
 
 End barrier_proto.
@@ -145,9 +137,9 @@ Section proof.
   Local Hint Resolve signal_step wait_step split_step : sts.
   Local Hint Resolve sts.closed_op : sts.
 
-  Hint Extern 50 (_ ∈ _) => set_solver : sts.
-  Hint Extern 50 (_ ⊆ _) => set_solver : sts.
-  Hint Extern 50 (_ ≡ _) => set_solver : sts.
+  Hint Extern 50 (_ ∈ _) => try rewrite !mkSet_elem_of; set_solver : sts.
+  Hint Extern 50 (_ ⊆ _) => try rewrite !mkSet_elem_of; set_solver : sts.
+  Hint Extern 50 (_ ≡ _) => try rewrite !mkSet_elem_of; set_solver : sts.
 
   Local Notation iProp := (iPropG heap_lang Σ).
 
@@ -293,20 +285,10 @@ Section proof.
       rewrite (sts_own_weaken ⊤ _ _ (i_states i ∩ low_states) _ 
                               ({[ Change i ]} ∪ {[ Send ]})).
       + apply pvs_mono. rewrite sts_ownS_op; eauto with sts.
-      (* TODO the rest of this proof is rather annoying. *)
-      + rewrite /= /tok /=. apply elem_of_equiv=>t.
-        rewrite elem_of_difference elem_of_union.
-        rewrite !mkSet_elem_of /change_tokens.
-        (* TODO: destruct t; set_solver does not work. What is the best way to do on? *)
-        destruct t as [i'|]; last by naive_solver. split.
-        * move=>[_ Hn]. left. destruct (decide (i = i')); first by subst i.
-          exfalso. apply Hn. left. set_solver.
-        * move=>[[EQ]|?]; last discriminate. set_solver. 
-      + apply elem_of_intersection. rewrite !mkSet_elem_of /=. set_solver.
-      + apply sts.closed_op; eauto with sts; [].
-        apply (non_empty_inhabited (State Low {[ i ]})).
-        apply elem_of_intersection.
-        rewrite !mkSet_elem_of /=. set_solver.
+      + rewrite /= /tok /=  =>t. rewrite !mkSet_elem_of.
+        move=>[[?]|?]; set_solver. 
+      + eauto with sts.
+      + eauto with sts.
   Qed.
 
   Lemma signal_spec l P (Φ : val → iProp) :
@@ -441,12 +423,7 @@ Section proof.
         do 2 rewrite !(assoc (★)%I) [(_ ★ sts_ownS _ _ _)%I]comm.
         rewrite -!assoc. rewrite [(sts_ownS _ _ _ ★ _ ★ _)%I]assoc -pvs_frame_r.
         apply sep_mono.
-        * rewrite -sts_ownS_op; [|by eauto with sts..].
-          apply sts_own_weaken; first done.
-          { rewrite !mkSet_elem_of /=. set_solver+. }
-          apply sts.closed_op; [by eauto with sts..|].
-          apply (non_empty_inhabited (State Low ({[i1]} ∪ ({[i2]} ∪ (I ∖ {[i]}))))).
-          rewrite !mkSet_elem_of /=. set_solver+.
+        * rewrite -sts_ownS_op; by eauto using sts_own_weaken with sts.
         * rewrite {1}[heap_ctx _]always_sep_dup !assoc [(_ ★ heap_ctx _)%I]comm -!assoc. apply sep_mono_r.
           rewrite !assoc ![(_ ★ heap_ctx _)%I]comm -!assoc. apply sep_mono_r.
           rewrite {1}[sts_ctx _ _ _]always_sep_dup !assoc [(_ ★ sts_ctx _ _ _)%I]comm -!assoc. apply sep_mono_r.
@@ -485,12 +462,7 @@ Section proof.
         do 2 rewrite !(assoc (★)%I) [(_ ★ sts_ownS _ _ _)%I]comm.
         rewrite -!assoc. rewrite [(sts_ownS _ _ _ ★ _ ★ _)%I]assoc -pvs_frame_r.
         apply sep_mono.
-        * rewrite -sts_ownS_op; [|by eauto with sts..].
-          apply sts_own_weaken; first done.
-          { rewrite !mkSet_elem_of /=. set_solver+. }
-          apply sts.closed_op; [by eauto with sts..|].
-          apply (non_empty_inhabited (State High ({[i1]} ∪ ({[i2]} ∪ (I ∖ {[i]}))))).
-          rewrite !mkSet_elem_of /=. set_solver+.
+        * rewrite -sts_ownS_op; by eauto using sts_own_weaken with sts.
         * rewrite {1}[heap_ctx _]always_sep_dup !assoc [(_ ★ heap_ctx _)%I]comm -!assoc. apply sep_mono_r.
           rewrite !assoc ![(_ ★ heap_ctx _)%I]comm -!assoc. apply sep_mono_r.
           rewrite {1}[sts_ctx _ _ _]always_sep_dup !assoc [(_ ★ sts_ctx _ _ _)%I]comm -!assoc. apply sep_mono_r.
diff --git a/program_logic/sts.v b/program_logic/sts.v
index e0e6c2ad11e64df9de2249217599c3d0051cb269..c794ce2731aee6044ef44afdd4df87d644342eb6 100644
--- a/program_logic/sts.v
+++ b/program_logic/sts.v
@@ -53,23 +53,15 @@ Section sts.
 
   (* The same rule as implication does *not* hold, as could be shown using
      sts_frag_included. *)
-  (* TODO: sts.closed forces the user to prove that S2 is inhabited. This is
-     silly, we know that S1 is inhabited since we own it, and hence S2 is
-     inhabited, too. Probably, sts.closed should really just be about closedness.
-     I think keeping disjointnes of the token stuff in there is fine, since it
-     does not incur any unnecessary side-conditions.
-     Then we additionally demand for validity that S is nonempty, rather than
-     making that part of "closed".
-   *)
   Lemma sts_ownS_weaken E γ S1 S2 T1 T2 :
-    T1 ≡ T2 → S1 ⊆ S2 → sts.closed S2 T2 →
+    T2 ⊆ T1 → S1 ⊆ S2 → sts.closed S2 T2 →
     sts_ownS γ S1 T1 ⊑ (|={E}=> sts_ownS γ S2 T2).
-  Proof. intros -> ? ?. by apply own_update, sts_update_frag. Qed.
+  Proof. intros ? ? ?. by apply own_update, sts_update_frag. Qed.
 
   Lemma sts_own_weaken E γ s S T1 T2 :
-    T1 ≡ T2 → s ∈ S → sts.closed S T2 →
+    T2 ⊆ T1 → s ∈ S → sts.closed S T2 →
     sts_own γ s T1 ⊑ (|={E}=> sts_ownS γ S T2).
-  Proof. intros -> ??. by apply own_update, sts_update_frag_up. Qed.
+  Proof. intros ???. by apply own_update, sts_update_frag_up. Qed.
 
   Lemma sts_ownS_op γ S1 S2 T1 T2 :
     T1 ∩ T2 ⊆ ∅ → sts.closed S1 T1 → sts.closed S2 T2 →
@@ -106,8 +98,9 @@ Section sts.
     rewrite -!assoc. apply const_elim_sep_l=> Hvalid.
     assert (s ∈ S) by (by eapply sts_auth_frag_valid_inv, discrete_valid).
     rewrite const_equiv // left_id comm sts_op_auth_frag //.
-    (* this is horrible, but will be fixed whenever we have RAs back *)
-    by rewrite -sts_frag_valid; eapply cmra_valid_op_r, discrete_valid.
+    assert (✓ sts_frag S T) as Hv by
+          by eapply cmra_valid_op_r, discrete_valid.
+    apply (Hv 0).
   Qed.
 
   Lemma sts_closing E γ s T s' T' :