diff --git a/algebra/upred.v b/algebra/upred.v
index 57fe1a7899ea70147c4fba7a4d5934ef1cdb583a..02bfe8cb6f64a18254e3e869af3dd02d98595996 100644
--- a/algebra/upred.v
+++ b/algebra/upred.v
@@ -708,10 +708,7 @@ Qed.
 Global Instance later_mono' : Proper ((⊑) ==> (⊑)) (@uPred_later M).
 Proof. intros P Q; apply later_mono. Qed.
 Lemma later_True : (▷ True : uPred M)%I ≡ True%I.
-Proof.
-  apply (anti_symm (⊑)); first done.
-  apply later_True'.
-Qed.
+Proof. apply (anti_symm (⊑)); auto using later_True'. Qed.
 Lemma later_impl P Q : ▷ (P → Q) ⊑ (▷ P → ▷ Q).
 Proof.
   apply impl_intro_l; rewrite -later_and.
diff --git a/algebra/upred_big_op.v b/algebra/upred_big_op.v
index 0c2d9876398dcd0118dfe764de7e4688772aebf5..5c8f4f055a4b2310c7c052472819591e16a1efa4 100644
--- a/algebra/upred_big_op.v
+++ b/algebra/upred_big_op.v
@@ -142,18 +142,15 @@ Section gmap.
   Lemma big_sepM_sepM P Q m :
     (Π★{map m} (λ i x, P i x ★ Q i x))%I ≡ (Π★{map m} P ★ Π★{map m} Q)%I.
   Proof.
-    rewrite /uPred_big_sepM. induction (map_to_list m); simpl;
-      first by rewrite right_id.
-    destruct a. rewrite IHl /= -!assoc. apply sep_proper; first done.
-    rewrite !assoc [(_ ★ Q _ _)%I]comm -!assoc. apply sep_proper; done.
+    rewrite /uPred_big_sepM.
+    induction (map_to_list m) as [|[i x] l IH]; csimpl; rewrite ?right_id //.
+    by rewrite IH -!assoc (assoc _ (Q _ _)) [(Q _ _ ★ _)%I]comm -!assoc.
   Qed.
-
-  Lemma big_sepM_later P m :
-    (Π★{map m} (λ i x, ▷ P i x))%I ≡ (▷ Π★{map m} P)%I.
+  Lemma big_sepM_later P m : (▷ Π★{map m} P)%I ≡ (Π★{map m} (λ i x, ▷ P i x))%I.
   Proof.
-    rewrite /uPred_big_sepM. induction (map_to_list m); simpl;
-      first by rewrite later_True.
-    destruct a. by rewrite IHl later_sep.
+    rewrite /uPred_big_sepM.
+    induction (map_to_list m) as [|[i x] l IH]; csimpl; rewrite ?later_True //.
+    by rewrite later_sep IH.
   Qed.
 End gmap.
 
@@ -205,18 +202,16 @@ Section gset.
   Lemma big_sepS_sepS P Q X :
     (Π★{set X} (λ x, P x ★ Q x))%I ≡ (Π★{set X} P ★ Π★{set X} Q)%I.
   Proof.
-    rewrite /uPred_big_sepS. induction (elements X); simpl;
-      first by rewrite right_id.
-    rewrite IHl -!assoc. apply uPred.sep_proper; first done.
-    rewrite !assoc [(_ ★ Q a)%I]comm -!assoc. apply sep_proper; done.
+    rewrite /uPred_big_sepS.
+    induction (elements X) as [|x l IH]; csimpl; first by rewrite ?right_id.
+    by rewrite IH -!assoc (assoc _ (Q _)) [(Q _ ★ _)%I]comm -!assoc.
   Qed.
 
-  Lemma big_sepS_later P X :
-    (Π★{set X} (λ x, ▷ P x))%I ≡ (▷ Π★{set X} P)%I.
+  Lemma big_sepS_later P X : (▷ Π★{set X} P)%I ≡ (Π★{set X} (λ x, ▷ P x))%I.
   Proof.
-    rewrite /uPred_big_sepS. induction (elements X); simpl;
-      first by rewrite later_True.
-    by rewrite IHl later_sep.
+    rewrite /uPred_big_sepS.
+    induction (elements X) as [|x l IH]; csimpl; first by rewrite ?later_True.
+    by rewrite later_sep IH.
   Qed.
 End gset.
 
diff --git a/barrier/barrier.v b/barrier/barrier.v
index 43ad8a574f222018010fe40b97c62c109588d1e0..1b605cc14e1a39500f7d923bed117563aab89afc 100644
--- a/barrier/barrier.v
+++ b/barrier/barrier.v
@@ -203,7 +203,7 @@ Section proof.
     (* Now we come to the core of the proof: Updating from waiting to ress. *)
     rewrite /waiting /ress sep_exist_l. apply exist_elim=>{Q} Q.
     rewrite later_wand {1}(later_intro P) !assoc wand_elim_r.
-    rewrite -big_sepS_later -big_sepS_sepS. apply big_sepS_mono'=>i.
+    rewrite big_sepS_later -big_sepS_sepS. apply big_sepS_mono'=>i.
     rewrite -(exist_intro (Q i)) comm. done.
   Qed.