diff --git a/algebra/agree.v b/algebra/agree.v
index d2d18766865b17a7ca6d9e66352d1e1292fa4833..7b8641655090fe0ed4fa5572b3ef863d2791b893 100644
--- a/algebra/agree.v
+++ b/algebra/agree.v
@@ -40,8 +40,8 @@ Proof.
     + by split.
     + by intros x y Hxy; split; intros; symmetry; apply Hxy; auto; apply Hxy.
     + intros x y z Hxy Hyz; split; intros n'; intros.
-      * transitivity (agree_is_valid y n'). by apply Hxy. by apply Hyz.
-      * transitivity (y n'). by apply Hxy. by apply Hyz, Hxy.
+      * trans (agree_is_valid y n'). by apply Hxy. by apply Hyz.
+      * trans (y n'). by apply Hxy. by apply Hyz, Hxy.
   - intros n x y Hxy; split; intros; apply Hxy; auto.
   - intros n c; apply and_wlog_r; intros;
       symmetry; apply (chain_cauchy c); naive_solver.
@@ -74,8 +74,8 @@ Proof.
   intros n x y1 y2 [Hy' Hy]; split; [|done].
   split; intros (?&?&Hxy); repeat (intro || split);
     try apply Hy'; eauto using agree_valid_le.
-  - etransitivity; [apply Hxy|apply Hy]; eauto using agree_valid_le.
-  - etransitivity; [apply Hxy|symmetry; apply Hy, Hy'];
+  - etrans; [apply Hxy|apply Hy]; eauto using agree_valid_le.
+  - etrans; [apply Hxy|symmetry; apply Hy, Hy'];
       eauto using agree_valid_le.
 Qed.
 Instance: Proper (dist n ==> dist n ==> dist n) (@op (agree A) _).
diff --git a/algebra/auth.v b/algebra/auth.v
index 9c78a1fd918e51a88faf30915be29c937e9144df..f64fa609038203b4b0c2011a92337a985b41d049 100644
--- a/algebra/auth.v
+++ b/algebra/auth.v
@@ -44,7 +44,7 @@ Proof.
   - intros n; split.
     + by intros ?; split.
     + by intros ?? [??]; split; symmetry.
-    + intros ??? [??] [??]; split; etransitivity; eauto.
+    + intros ??? [??] [??]; split; etrans; eauto.
   - by intros ? [??] [??] [??]; split; apply dist_S.
   - intros n c; split. apply (conv_compl n (chain_map authoritative c)).
     apply (conv_compl n (chain_map own c)).
diff --git a/algebra/cmra.v b/algebra/cmra.v
index 534341d7e0f1e764c21b5afbac3d774be0df69e8..5d61df86a84159d9c36797b5171907338140796f 100644
--- a/algebra/cmra.v
+++ b/algebra/cmra.v
@@ -250,7 +250,7 @@ Qed.
 Global Instance cmra_included_preorder: PreOrder (@included A _ _).
 Proof.
   split; red; intros until 0; rewrite !cmra_included_includedN; first done.
-  intros; etransitivity; eauto.
+  intros; etrans; eauto.
 Qed.
 Lemma cmra_validN_includedN n x y : ✓{n} y → x ≼{n} y → ✓{n} x.
 Proof. intros Hyv [z ?]; cofe_subst y; eauto using cmra_validN_op_l. Qed.
@@ -391,7 +391,7 @@ Section identity_updates.
   Lemma cmra_update_empty x : x ~~> ∅.
   Proof. intros n z; rewrite left_id; apply cmra_validN_op_r. Qed.
   Lemma cmra_update_empty_alt y : ∅ ~~> y ↔ ∀ x, x ~~> y.
-  Proof. split; [intros; transitivity ∅|]; auto using cmra_update_empty. Qed.
+  Proof. split; [intros; trans ∅|]; auto using cmra_update_empty. Qed.
 End identity_updates.
 End cmra.
 
diff --git a/algebra/cmra_big_op.v b/algebra/cmra_big_op.v
index 74386451aa1288b1a40e6ac9905ae1fc8405bd6d..3082e1a5fa5334f6be290eec779edb58061a86f8 100644
--- a/algebra/cmra_big_op.v
+++ b/algebra/cmra_big_op.v
@@ -23,7 +23,7 @@ Proof.
   induction 1 as [|x xs1 xs2 ? IH|x y xs|xs1 xs2 xs3]; simpl; auto.
   - by rewrite IH.
   - by rewrite !assoc (comm _ x).
-  - by transitivity (big_op xs2).
+  - by trans (big_op xs2).
 Qed.
 Global Instance big_op_proper : Proper ((≡) ==> (≡)) big_op.
 Proof. by induction 1; simpl; repeat apply (_ : Proper (_ ==> _ ==> _) op). Qed.
diff --git a/algebra/cofe.v b/algebra/cofe.v
index 4bdb3007b93c6e608bb53a2d5c17ae8d3d5b3994..048ce91533386c9af32748829f65b92ab95624fd 100644
--- a/algebra/cofe.v
+++ b/algebra/cofe.v
@@ -99,13 +99,13 @@ Section cofe.
     split.
     - by intros x; rewrite equiv_dist.
     - by intros x y; rewrite !equiv_dist.
-    - by intros x y z; rewrite !equiv_dist; intros; transitivity y.
+    - by intros x y z; rewrite !equiv_dist; intros; trans y.
   Qed.
   Global Instance dist_ne n : Proper (dist n ==> dist n ==> iff) (@dist A _ n).
   Proof.
     intros x1 x2 ? y1 y2 ?; split; intros.
-    - by transitivity x1; [|transitivity y1].
-    - by transitivity x2; [|transitivity y2].
+    - by trans x1; [|trans y1].
+    - by trans x2; [|trans y2].
   Qed.
   Global Instance dist_proper n : Proper ((≡) ==> (≡) ==> iff) (@dist A _ n).
   Proof.
@@ -217,7 +217,7 @@ Section cofe_mor.
     - intros n; split.
       + by intros f x.
       + by intros f g ? x.
-      + by intros f g h ?? x; transitivity (g x).
+      + by intros f g h ?? x; trans (g x).
     - by intros n f g ? x; apply dist_S.
     - intros n c x; simpl.
       by rewrite (conv_compl n (fun_chain c x)) /=.
@@ -352,7 +352,7 @@ Section later.
     - intros [|n]; [by split|split]; unfold dist, later_dist.
       + by intros [x].
       + by intros [x] [y].
-      + by intros [x] [y] [z] ??; transitivity y.
+      + by intros [x] [y] [z] ??; trans y.
     - intros [|n] [x] [y] ?; [done|]; unfold dist, later_dist; by apply dist_S.
     - intros [|n] c; [done|by apply (conv_compl n (later_chain c))].
   Qed.
diff --git a/algebra/cofe_solver.v b/algebra/cofe_solver.v
index dac844a640414f988b547c4daa995d4ca9e384d1..793f2c312e198d3677162e1eea8f2c09baf6dbd1 100644
--- a/algebra/cofe_solver.v
+++ b/algebra/cofe_solver.v
@@ -71,7 +71,7 @@ Proof.
   - intros k; split.
     + by intros X n.
     + by intros X Y ? n.
-    + by intros X Y Z ?? n; transitivity (Y n).
+    + by intros X Y Z ?? n; trans (Y n).
   - intros k X Y HXY n; apply dist_S.
     by rewrite -(g_tower X) (HXY (S n)) g_tower.
   - intros n c k; rewrite /= (conv_compl n (tower_chain c k)).
@@ -209,7 +209,7 @@ Proof.
   - move=> X /=.
     rewrite equiv_dist; intros n k; unfold unfold, fold; simpl.
     rewrite -g_tower -(gg_tower _ n); apply (_ : Proper (_ ==> _) (g _)).
-    transitivity (map (ff n, gg n) (X (S (n + k)))).
+    trans (map (ff n, gg n) (X (S (n + k)))).
     { rewrite /unfold (conv_compl n (unfold_chain X)).
       rewrite -(chain_cauchy (unfold_chain X) n (S (n + k))) /=; last lia.
       rewrite -(dist_le _ _ _ _ (f_tower (n + k) _)); last lia.
@@ -234,6 +234,6 @@ Proof.
     apply (contractive_ne map); split => Y /=.
     + apply dist_le with n; last omega.
       rewrite f_tower. apply dist_S. by rewrite embed_tower.
-    + etransitivity; [apply embed_ne, equiv_dist, g_tower|apply embed_tower].
+    + etrans; [apply embed_ne, equiv_dist, g_tower|apply embed_tower].
 Qed.
 End solver. End solver.
diff --git a/algebra/dra.v b/algebra/dra.v
index a6ef06249b153a1109e69488cf0423f5c6a40de0..22183991bb352a74d4196a37b33dcec680ec2397 100644
--- a/algebra/dra.v
+++ b/algebra/dra.v
@@ -60,7 +60,7 @@ Proof.
   - by intros [x px ?]; simpl.
   - intros [x px ?] [y py ?]; naive_solver.
   - intros [x px ?] [y py ?] [z pz ?] [? Hxy] [? Hyz]; simpl in *.
-    split; [|intros; transitivity y]; tauto.
+    split; [|intros; trans y]; tauto.
 Qed.
 Instance dra_valid_proper' : Proper ((≡) ==> iff) (valid : A → Prop).
 Proof. by split; apply dra_valid_proper. Qed.
diff --git a/algebra/excl.v b/algebra/excl.v
index c340c72458e9e8aec0147d3c07fc792975733a2f..58298171440115c97b2385a3dc9d0e7f78684394 100644
--- a/algebra/excl.v
+++ b/algebra/excl.v
@@ -56,7 +56,7 @@ Proof.
   - intros n; split.
     + by intros [x| |]; constructor.
     + by destruct 1; constructor.
-    + destruct 1; inversion_clear 1; constructor; etransitivity; eauto.
+    + destruct 1; inversion_clear 1; constructor; etrans; eauto.
   - by inversion_clear 1; constructor; apply dist_S.
   - intros n c; unfold compl, excl_compl.
     destruct (Some_dec (maybe Excl (c 1))) as [[x Hx]|].
diff --git a/algebra/fin_maps.v b/algebra/fin_maps.v
index 0a16ba1d2a5b51caa15587c64952383a600cffeb..92714de8da2598d03936a11aff57714e4f46e793 100644
--- a/algebra/fin_maps.v
+++ b/algebra/fin_maps.v
@@ -22,7 +22,7 @@ Proof.
   - intros n; split.
     + by intros m k.
     + by intros m1 m2 ? k.
-    + by intros m1 m2 m3 ?? k; transitivity (m2 !! k).
+    + by intros m1 m2 m3 ?? k; trans (m2 !! k).
   - by intros n m1 m2 ? k; apply dist_S.
   - intros n c k; rewrite /compl /map_compl lookup_imap.
     feed inversion (λ H, chain_cauchy c 0 (S n) H k); simpl; auto with lia.
diff --git a/algebra/iprod.v b/algebra/iprod.v
index 8b46f6293b1a41f86412a7f07e2f640108e6479e..18c272406d979c657f7f7528cdc6053143eb3afe 100644
--- a/algebra/iprod.v
+++ b/algebra/iprod.v
@@ -35,7 +35,7 @@ Section iprod_cofe.
     - intros n; split.
       + by intros f x.
       + by intros f g ? x.
-      + by intros f g h ?? x; transitivity (g x).
+      + by intros f g h ?? x; trans (g x).
     - intros n f g Hfg x; apply dist_S, Hfg.
     - intros n c x.
       rewrite /compl /iprod_compl (conv_compl n (iprod_chain c x)).
diff --git a/algebra/option.v b/algebra/option.v
index 777219d00e2bd3a8133e438367af51be4d91eb06..7ae362ec1683bbf0997c2f1d4594cc59fa16f33f 100644
--- a/algebra/option.v
+++ b/algebra/option.v
@@ -29,7 +29,7 @@ Proof.
   - intros n; split.
     + by intros [x|]; constructor.
     + by destruct 1; constructor.
-    + destruct 1; inversion_clear 1; constructor; etransitivity; eauto.
+    + destruct 1; inversion_clear 1; constructor; etrans; eauto.
   - by inversion_clear 1; constructor; apply dist_S.
   - intros n c; unfold compl, option_compl.
     destruct (Some_dec (c 1)) as [[x Hx]|].
diff --git a/algebra/sts.v b/algebra/sts.v
index 6180165d07c0215189010c9a9dd5c9392811efdf..9a35709b4cbb8fdde6643f0fb111598994634057 100644
--- a/algebra/sts.v
+++ b/algebra/sts.v
@@ -224,7 +224,7 @@ Proof.
   split.
   - by intros []; constructor.
   - by destruct 1; constructor.
-  - destruct 1; inversion_clear 1; constructor; etransitivity; eauto.
+  - destruct 1; inversion_clear 1; constructor; etrans; eauto.
 Qed.
 Global Instance sts_dra : DRA (car sts).
 Proof.
@@ -366,7 +366,7 @@ Lemma sts_op_frag S1 S2 T1 T2 :
 Proof.
   intros HT HS1 HS2. rewrite /sts_frag.
   (* FIXME why does rewrite not work?? *)
-  etransitivity; last eapply to_validity_op; try done; [].
+  etrans; last eapply to_validity_op; try done; [].
   intros Hval. constructor; last set_solver. eapply closed_ne, Hval.
 Qed.
 
diff --git a/algebra/upred.v b/algebra/upred.v
index 2ff77de116bbe5e8a79cec5db0789c4b9b9c2db9..4c9080f72a61c1b9d40898ab817201fefa25a7ff 100644
--- a/algebra/upred.v
+++ b/algebra/upred.v
@@ -1,6 +1,6 @@
 From algebra Require Export cmra.
-Local Hint Extern 1 (_ ≼ _) => etransitivity; [eassumption|].
-Local Hint Extern 1 (_ ≼ _) => etransitivity; [|eassumption].
+Local Hint Extern 1 (_ ≼ _) => etrans; [eassumption|].
+Local Hint Extern 1 (_ ≼ _) => etrans; [|eassumption].
 Local Hint Extern 10 (_ ≤ _) => omega.
 
 Record uPred (M : cmraT) : Type := IProp {
@@ -40,7 +40,7 @@ Section cofe.
     - intros n; split.
       + by intros P x i.
       + by intros P Q HPQ x i ??; symmetry; apply HPQ.
-      + by intros P Q Q' HP HQ i x ??; transitivity (Q i x);[apply HP|apply HQ].
+      + by intros P Q Q' HP HQ i x ??; trans (Q i x);[apply HP|apply HQ].
     - intros n P Q HPQ i x ??; apply HPQ; auto.
     - intros n c i x ??; symmetry; apply (chain_cauchy c i (S n)); auto.
   Qed.
@@ -243,8 +243,8 @@ Global Instance entails_proper :
   Proper ((≡) ==> (≡) ==> iff) ((⊑) : relation (uPred M)).
 Proof.
   move => P1 P2 /equiv_spec [HP1 HP2] Q1 Q2 /equiv_spec [HQ1 HQ2]; split; intros.
-  - by transitivity P1; [|transitivity Q1].
-  - by transitivity P2; [|transitivity Q2].
+  - by trans P1; [|trans Q1].
+  - by trans P2; [|trans Q2].
 Qed.
 
 (** Non-expansiveness and setoid morphisms *)
@@ -734,7 +734,7 @@ Proof. by rewrite /uPred_iff later_and !later_impl. Qed.
 Lemma löb_strong P Q : (P ∧ ▷Q) ⊑ Q → P ⊑ Q.
 Proof.
   intros Hlöb. apply impl_entails.
-  etransitivity; last by eapply löb.
+  etrans; last by eapply löb.
   apply impl_intro_l, impl_intro_l. rewrite right_id -{2}Hlöb.
   apply and_intro; first by eauto.
   by rewrite {1}(later_intro P) later_impl impl_elim_r.
diff --git a/algebra/upred_big_op.v b/algebra/upred_big_op.v
index ae1dea030d45f256c6859cd6b27ef16fe94f9834..b8ac2cd8f66b7d8f2c644f97a15af3009e160b9a 100644
--- a/algebra/upred_big_op.v
+++ b/algebra/upred_big_op.v
@@ -61,14 +61,14 @@ Proof.
   induction 1 as [|P Ps Qs ? IH|P Q Ps|]; simpl; auto.
   - by rewrite IH.
   - by rewrite !assoc (comm _ P).
-  - etransitivity; eauto.
+  - etrans; eauto.
 Qed.
 Global Instance big_sep_perm : Proper ((≡ₚ) ==> (≡)) (@uPred_big_sep M).
 Proof.
   induction 1 as [|P Ps Qs ? IH|P Q Ps|]; simpl; auto.
   - by rewrite IH.
   - by rewrite !assoc (comm _ P).
-  - etransitivity; eauto.
+  - etrans; eauto.
 Qed.
 
 Lemma big_and_app Ps Qs : (Π∧ (Ps ++ Qs))%I ≡ (Π∧ Ps ∧ Π∧ Qs)%I.
@@ -103,7 +103,7 @@ Section gmap.
     m2 ⊆ m1 → (∀ x k, m2 !! k = Some x → Φ k x ⊑ Ψ k x) →
     (Π★{map m1} Φ) ⊑ (Π★{map m2} Ψ).
   Proof.
-    intros HX HΦ. transitivity (Π★{map m2} Φ)%I.
+    intros HX HΦ. trans (Π★{map m2} Φ)%I.
     - by apply big_sep_contains, fmap_contains, map_to_list_contains.
     - apply big_sep_mono', Forall2_fmap, Forall2_Forall.
       apply Forall_forall=> -[i x] ? /=. by apply HΦ, elem_of_map_to_list.
@@ -163,7 +163,7 @@ Section gset.
   Lemma big_sepS_mono Φ Ψ X Y :
     Y ⊆ X → (∀ x, x ∈ Y → Φ x ⊑ Ψ x) → (Π★{set X} Φ) ⊑ (Π★{set Y} Ψ).
   Proof.
-    intros HX HΦ. transitivity (Π★{set Y} Φ)%I.
+    intros HX HΦ. trans (Π★{set Y} Φ)%I.
     - by apply big_sep_contains, fmap_contains, elements_contains.
     - apply big_sep_mono', Forall2_fmap, Forall2_Forall.
       apply Forall_forall=> x ? /=. by apply HΦ, elem_of_elements.
diff --git a/barrier/barrier.v b/barrier/barrier.v
index 1765e0820f5cb04b2e3317501d3592a1533e0d0d..453d1bd9f55cf8e1380129821e6cee228a1ad2d7 100644
--- a/barrier/barrier.v
+++ b/barrier/barrier.v
@@ -157,7 +157,7 @@ Section proof.
     { by eapply (saved_prop_alloc _ P). }
     rewrite pvs_frame_l. apply pvs_strip_pvs. rewrite sep_exist_l.
     apply exist_elim=>i.
-    transitivity (pvs ⊤ ⊤ (heap_ctx heapN ★ ▷ (barrier_inv l P (State Low {[ i ]}))  ★ saved_prop_own i P)).
+    trans (pvs ⊤ ⊤ (heap_ctx heapN ★ ▷ (barrier_inv l P (State Low {[ i ]}))  ★ saved_prop_own i P)).
     - rewrite -pvs_intro. rewrite [(_ ★ heap_ctx _)%I]comm -!assoc. apply sep_mono_r.
       rewrite {1}[saved_prop_own _ _]always_sep_dup !assoc. apply sep_mono_l.
       rewrite /barrier_inv /waiting -later_intro. apply sep_mono_r.
@@ -215,7 +215,7 @@ Section proof.
     apply const_elim_sep_l=>Hs. destruct p; last done.
     rewrite {1}/barrier_inv =>/={Hs}. rewrite later_sep.
     eapply wp_store; eauto with I ndisj.
-    rewrite -!assoc. apply sep_mono_r. etransitivity; last eapply later_mono.
+    rewrite -!assoc. apply sep_mono_r. etrans; last eapply later_mono.
     { (* Is this really the best way to strip the later? *)
       erewrite later_sep. apply sep_mono_r. apply later_intro. }
     apply wand_intro_l. rewrite -(exist_intro (State High I)).
@@ -256,7 +256,7 @@ Section proof.
     apply const_elim_sep_l=>Hs.
     rewrite {1}/barrier_inv =>/=. rewrite later_sep.
     eapply wp_load; eauto with I ndisj.
-    rewrite -!assoc. apply sep_mono_r. etransitivity; last eapply later_mono.
+    rewrite -!assoc. apply sep_mono_r. etrans; last eapply later_mono.
     { (* Is this really the best way to strip the later? *)
       erewrite later_sep. apply sep_mono_r. rewrite !assoc. erewrite later_sep.
       apply sep_mono_l, later_intro. }
@@ -294,7 +294,7 @@ Section proof.
     rewrite [(sts_own _ _ _ ★ _)%I]sep_elim_r [(sts_ctx _ _ _ ★ _)%I]sep_elim_r.
     rewrite !assoc [(_ ★ saved_prop_own i Q)%I]comm !assoc saved_prop_agree.
     wp_op>; last done. intros _.
-    etransitivity; last eapply later_mono.
+    etrans; last eapply later_mono.
     { (* Is this really the best way to strip the later? *)
       erewrite later_sep. apply sep_mono; last apply later_intro.
       rewrite ->later_sep. apply sep_mono_l. rewrite ->later_sep. done. }
diff --git a/heap_lang/heap.v b/heap_lang/heap.v
index 9314bf11ff003900fe529a90b389dc2817d1f656..5d66586d4b7daa46bd4db0b74ebe0650ed1acee5 100644
--- a/heap_lang/heap.v
+++ b/heap_lang/heap.v
@@ -67,7 +67,7 @@ Section heap.
     authG heap_lang Σ heapRA → nclose N ⊆ E →
     ownP σ ⊑ (|={E}=> ∃ _ : heapG Σ, heap_ctx N ∧ Π★{map σ} heap_mapsto).
   Proof.
-    intros. rewrite -{1}(from_to_heap σ). etransitivity.
+    intros. rewrite -{1}(from_to_heap σ). etrans.
     { rewrite [ownP _]later_intro.
       apply (auth_alloc (ownP ∘ of_heap) E N (to_heap σ)); last done.
       apply to_heap_valid. }
@@ -103,7 +103,7 @@ Section heap.
     P ⊑ || Alloc e @ E {{ Φ }}.
   Proof.
     rewrite /heap_ctx /heap_inv /heap_mapsto=> ?? Hctx HP.
-    transitivity (|={E}=> auth_own heap_name ∅ ★ P)%I.
+    trans (|={E}=> auth_own heap_name ∅ ★ P)%I.
     { by rewrite -pvs_frame_r -(auth_empty _ E) left_id. }
     apply wp_strip_pvs, (auth_fsa heap_inv (wp_fsa (Alloc e)))
       with N heap_name ∅; simpl; eauto with I.
diff --git a/heap_lang/wp_tactics.v b/heap_lang/wp_tactics.v
index 3356f91ca7686c6341dafae3557b6a03764a5865..87bd4afcb9d4746bcb6c0b11601918b2d37a488c 100644
--- a/heap_lang/wp_tactics.v
+++ b/heap_lang/wp_tactics.v
@@ -13,19 +13,19 @@ Ltac wp_strip_later :=
     | |- _ ⊑ ▷ _ => apply later_intro
     | |- _ ⊑ _ => reflexivity
     end
-  in revert_intros ltac:(etransitivity; [|go]).
+  in revert_intros ltac:(etrans; [|go]).
 
 Ltac wp_bind K :=
   lazymatch eval hnf in K with
   | [] => idtac
-  | _ => etransitivity; [|solve [ apply (wp_bind K) ]]; simpl
+  | _ => etrans; [|solve [ apply (wp_bind K) ]]; simpl
   end.
 Ltac wp_finish :=
   let rec go :=
   match goal with
-  | |- _ ⊑ ▷ _ => etransitivity; [|apply later_mono; go; reflexivity]
+  | |- _ ⊑ ▷ _ => etrans; [|apply later_mono; go; reflexivity]
   | |- _ ⊑ wp _ _ _ =>
-     etransitivity; [|eapply wp_value_pvs; reflexivity];
+     etrans; [|eapply wp_value_pvs; reflexivity];
      (* sometimes, we will have to do a final view shift, so only apply
      wp_value if we obtain a consecutive wp *)
      try (eapply pvs_intro;
@@ -38,7 +38,7 @@ Tactic Notation "wp_rec" ">" :=
   | |- _ ⊑ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
     match eval cbv in e' with
     | App (Rec _ _ _) _ =>
-       wp_bind K; etransitivity; [|eapply wp_rec; reflexivity]; wp_finish
+       wp_bind K; etrans; [|eapply wp_rec; reflexivity]; wp_finish
     end)
   end.
 Tactic Notation "wp_rec" := wp_rec>; wp_strip_later.
@@ -48,7 +48,7 @@ Tactic Notation "wp_lam" ">" :=
   | |- _ ⊑ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
     match eval cbv in e' with
     | App (Rec "" _ _) _ =>
-       wp_bind K; etransitivity; [|eapply wp_lam; reflexivity]; wp_finish
+       wp_bind K; etrans; [|eapply wp_lam; reflexivity]; wp_finish
     end)
   end.
 Tactic Notation "wp_lam" := wp_lam>; wp_strip_later.
@@ -66,9 +66,9 @@ Tactic Notation "wp_op" ">" :=
     | BinOp LeOp _ _ => wp_bind K; apply wp_le; wp_finish
     | BinOp EqOp _ _ => wp_bind K; apply wp_eq; wp_finish
     | BinOp _ _ _ =>
-       wp_bind K; etransitivity; [|eapply wp_bin_op; reflexivity]; wp_finish
+       wp_bind K; etrans; [|eapply wp_bin_op; reflexivity]; wp_finish
     | UnOp _ _ =>
-       wp_bind K; etransitivity; [|eapply wp_un_op; reflexivity]; wp_finish
+       wp_bind K; etrans; [|eapply wp_un_op; reflexivity]; wp_finish
     end)
   end.
 Tactic Notation "wp_op" := wp_op>; wp_strip_later.
@@ -79,7 +79,7 @@ Tactic Notation "wp_if" ">" :=
     match eval cbv in e' with
     | If _ _ _ =>
        wp_bind K;
-       etransitivity; [|apply wp_if_true || apply wp_if_false]; wp_finish
+       etrans; [|apply wp_if_true || apply wp_if_false]; wp_finish
     end)
   end.
 Tactic Notation "wp_if" := wp_if>; wp_strip_later.
@@ -97,5 +97,5 @@ Tactic Notation "wp" ">" tactic(tac) :=
 Tactic Notation "wp" tactic(tac) := (wp> tac); wp_strip_later.
 
 (* In case the precondition does not match *)
-Tactic Notation "ewp" tactic(tac) := wp (etransitivity; [|tac]).
-Tactic Notation "ewp" ">" tactic(tac) := wp> (etransitivity; [|tac]).
+Tactic Notation "ewp" tactic(tac) := wp (etrans; [|tac]).
+Tactic Notation "ewp" ">" tactic(tac) := wp> (etrans; [|tac]).
diff --git a/prelude/fin_map_dom.v b/prelude/fin_map_dom.v
index 55e575f61fc0d34d8a18751c6eb8d42cbb0adb4d..0d735863b03dcbf01e7624f3d6f73ef41f4b6a01 100644
--- a/prelude/fin_map_dom.v
+++ b/prelude/fin_map_dom.v
@@ -60,7 +60,7 @@ Lemma dom_insert_subseteq {A} (m : M A) i x : dom D m ⊆ dom D (<[i:=x]>m).
 Proof. rewrite (dom_insert _). set_solver. Qed.
 Lemma dom_insert_subseteq_compat_l {A} (m : M A) i x X :
   X ⊆ dom D m → X ⊆ dom D (<[i:=x]>m).
-Proof. intros. transitivity (dom D m); eauto using dom_insert_subseteq. Qed.
+Proof. intros. trans (dom D m); eauto using dom_insert_subseteq. Qed.
 Lemma dom_singleton {A} (i : K) (x : A) : dom D {[i := x]} ≡ {[ i ]}.
 Proof. rewrite <-insert_empty, dom_insert, dom_empty; set_solver. Qed.
 Lemma dom_delete {A} (m : M A) i : dom D (delete i m) ≡ dom D m ∖ {[ i ]}.
diff --git a/prelude/fin_maps.v b/prelude/fin_maps.v
index 0f3ec1cbbcec2aae19542fad18021a07cd765dbd..c09dc4125881dd3eb29c3e694dcb7a9368b19ec6 100644
--- a/prelude/fin_maps.v
+++ b/prelude/fin_maps.v
@@ -123,7 +123,7 @@ Section setoid.
     split.
     - by intros m i.
     - by intros m1 m2 ? i.
-    - by intros m1 m2 m3 ?? i; transitivity (m2 !! i).
+    - by intros m1 m2 m3 ?? i; trans (m2 !! i).
   Qed.
   Global Instance lookup_proper (i : K) :
     Proper ((≡) ==> (≡)) (lookup (M:=M A) i).
@@ -199,7 +199,7 @@ Proof.
   split; [intros m i; by destruct (m !! i); simpl|].
   intros m1 m2 m3 Hm12 Hm23 i; specialize (Hm12 i); specialize (Hm23 i).
   destruct (m1 !! i), (m2 !! i), (m3 !! i); simplify_eq/=;
-    done || etransitivity; eauto.
+    done || etrans; eauto.
 Qed.
 Global Instance: PartialOrder ((⊆) : relation (M A)).
 Proof.
@@ -1182,10 +1182,10 @@ Proof.
   intros. rewrite map_union_comm by done. by apply map_union_subseteq_l.
 Qed.
 Lemma map_union_subseteq_l_alt {A} (m1 m2 m3 : M A) : m1 ⊆ m2 → m1 ⊆ m2 ∪ m3.
-Proof. intros. transitivity m2; auto using map_union_subseteq_l. Qed.
+Proof. intros. trans m2; auto using map_union_subseteq_l. Qed.
 Lemma map_union_subseteq_r_alt {A} (m1 m2 m3 : M A) :
   m2 ⊥ₘ m3 → m1 ⊆ m3 → m1 ⊆ m2 ∪ m3.
-Proof. intros. transitivity m3; auto using map_union_subseteq_r. Qed.
+Proof. intros. trans m3; auto using map_union_subseteq_r. Qed.
 Lemma map_union_preserving_l {A} (m1 m2 m3 : M A) : m1 ⊆ m2 → m3 ∪ m1 ⊆ m3 ∪ m2.
 Proof.
   rewrite !map_subseteq_spec. intros ???.
diff --git a/prelude/lexico.v b/prelude/lexico.v
index fdeca6a58cc271a9c69fcc00b242ea4ebbcb79aa..1b92f9825d5cc13de58f467b6f8ce0295afbda05 100644
--- a/prelude/lexico.v
+++ b/prelude/lexico.v
@@ -42,7 +42,7 @@ Lemma prod_lexico_transitive `{Lexico A, Lexico B, !Transitive (@lexico A _)}
 Proof.
   intros Hx12 Hx23 ?; revert Hx12 Hx23. unfold lexico, prod_lexico.
   intros [|[??]] [?|[??]]; simplify_eq/=; auto.
-  by left; transitivity x2.
+  by left; trans x2.
 Qed.
 
 Instance prod_lexico_po `{Lexico A, Lexico B, !StrictOrder (@lexico A _)}
@@ -52,7 +52,7 @@ Proof.
   - intros [x y]. apply prod_lexico_irreflexive.
     by apply (irreflexivity lexico y).
   - intros [??] [??] [??] ??.
-    eapply prod_lexico_transitive; eauto. apply transitivity.
+    eapply prod_lexico_transitive; eauto. apply trans.
 Qed.
 Instance prod_lexico_trichotomyT `{Lexico A, tA : !TrichotomyT (@lexico A _)}
   `{Lexico B, tB : !TrichotomyT (@lexico B _)}: TrichotomyT (@lexico (A * B) _).
@@ -143,7 +143,7 @@ Instance sig_lexico_po `{Lexico A, !StrictOrder (@lexico A _)}
 Proof.
   unfold lexico, sig_lexico. split.
   - intros [x ?] ?. by apply (irreflexivity lexico x). 
-  - intros [x1 ?] [x2 ?] [x3 ?] ??. by transitivity x2.
+  - intros [x1 ?] [x2 ?] [x3 ?] ??. by trans x2.
 Qed.
 Instance sig_lexico_trichotomy `{Lexico A, tA : !TrichotomyT (@lexico A _)}
   (P : A → Prop) `{∀ x, ProofIrrel (P x)} : TrichotomyT (@lexico (sig P) _).
diff --git a/prelude/list.v b/prelude/list.v
index b47850c163641e05ab620b6c24e68f2436611e3d..8541aa18ced733122230d68af2296ea17d516b8b 100644
--- a/prelude/list.v
+++ b/prelude/list.v
@@ -371,7 +371,7 @@ Section setoid.
     - intros l; induction l; constructor; auto.
     - induction 1; constructor; auto.
     - intros l1 l2 l3 Hl; revert l3.
-      induction Hl; inversion_clear 1; constructor; try etransitivity; eauto.
+      induction Hl; inversion_clear 1; constructor; try etrans; eauto.
   Qed.
   Global Instance cons_proper : Proper ((≡) ==> (≡) ==> (≡)) (@cons A).
   Proof. by constructor. Qed.
@@ -1719,7 +1719,7 @@ Proof. revert i. by induction l; intros [|?]; simpl; constructor. Qed.
 Lemma sublist_foldr_delete l is : foldr delete l is `sublist` l.
 Proof.
   induction is as [|i is IH]; simpl; [done |].
-  transitivity (foldr delete l is); auto using sublist_delete.
+  trans (foldr delete l is); auto using sublist_delete.
 Qed.
 Lemma sublist_alt l1 l2 : l1 `sublist` l2 ↔ ∃ is, l1 = foldr delete l2 is.
 Proof.
@@ -1749,7 +1749,7 @@ Proof.
     + by rewrite !Permutation_middle, Permutation_swap.
   - intros l3 ?. destruct (IH2 l3) as (l3'&?&?); trivial.
     destruct (IH1 l3') as (l3'' &?&?); trivial. exists l3''.
-    split. done. etransitivity; eauto.
+    split. done. etrans; eauto.
 Qed.
 Lemma sublist_Permutation l1 l2 l3 :
   l1 `sublist` l2 → l2 ≡ₚ l3 → ∃ l4, l1 ≡ₚ l4 ∧ l4 `sublist` l3.
@@ -1770,7 +1770,7 @@ Proof.
     + exists (x :: y :: l1''). by repeat constructor.
   - intros l1 ?. destruct (IH1 l1) as (l3'&?&?); trivial.
     destruct (IH2 l3') as (l3'' &?&?); trivial. exists l3''.
-    split; [|done]. etransitivity; eauto.
+    split; [|done]. etrans; eauto.
 Qed.
 
 (** Properties of the [contains] predicate *)
@@ -1816,10 +1816,10 @@ Proof. intro. apply contains_Permutation_length_le. lia. Qed.
 Global Instance: Proper ((≡ₚ) ==> (≡ₚ) ==> iff) (@contains A).
 Proof.
   intros l1 l2 ? k1 k2 ?. split; intros.
-  - transitivity l1. by apply Permutation_contains.
-    transitivity k1. done. by apply Permutation_contains.
-  - transitivity l2. by apply Permutation_contains.
-    transitivity k2. done. by apply Permutation_contains.
+  - trans l1. by apply Permutation_contains.
+    trans k1. done. by apply Permutation_contains.
+  - trans l2. by apply Permutation_contains.
+    trans k2. done. by apply Permutation_contains.
 Qed.
 Global Instance: AntiSymm (≡ₚ) (@contains A).
 Proof. red. auto using contains_Permutation_length_le, contains_length. Qed.
@@ -1842,9 +1842,9 @@ Proof.
     - intros x l1 l3 ? (l2&?&?). exists (x :: l2). by repeat constructor.
     - intros l1 l3 l5 ? (l2&?&?) ? (l4&?&?).
       destruct (Permutation_sublist l2 l3 l4) as (l3'&?&?); trivial.
-      exists l3'. split; etransitivity; eauto. }
+      exists l3'. split; etrans; eauto. }
   intros (l2&?&?).
-  transitivity l2; auto using sublist_contains, Permutation_contains.
+  trans l2; auto using sublist_contains, Permutation_contains.
 Qed.
 Lemma contains_sublist_r l1 l3 :
   l1 `contains` l3 ↔ ∃ l2, l1 ≡ₚ l2 ∧ l2 `sublist` l3.
@@ -1863,7 +1863,7 @@ Proof. rewrite !(comm (++) _ k). apply contains_skips_l. Qed.
 Lemma contains_app l1 l2 k1 k2 :
   l1 `contains` l2 → k1 `contains` k2 → l1 ++ k1 `contains` l2 ++ k2.
 Proof.
-  transitivity (l1 ++ k2); auto using contains_skips_l, contains_skips_r.
+  trans (l1 ++ k2); auto using contains_skips_l, contains_skips_r.
 Qed.
 Lemma contains_cons_r x l k :
   l `contains` x :: k ↔ l `contains` k ∨ ∃ l', l ≡ₚ x :: l' ∧ l' `contains` k.
@@ -1975,7 +1975,7 @@ Section contains_dec.
     - simplify_option_eq; eauto using Permutation_swap.
     - destruct (IH1 k1) as (k2&?&?); trivial.
       destruct (IH2 k2) as (k3&?&?); trivial.
-      exists k3. split; eauto. by transitivity k2.
+      exists k3. split; eauto. by trans k2.
   Qed.
   Lemma list_remove_Some l k x : list_remove x l = Some k → l ≡ₚ x :: k.
   Proof.
@@ -2493,7 +2493,7 @@ Section Forall2_order.
   Global Instance: Symmetric R → Symmetric (Forall2 R).
   Proof. intros. induction 1; constructor; auto. Qed.
   Global Instance: Transitive R → Transitive (Forall2 R).
-  Proof. intros ????. apply Forall2_transitive. by apply @transitivity. Qed.
+  Proof. intros ????. apply Forall2_transitive. by apply @trans. Qed.
   Global Instance: Equivalence R → Equivalence (Forall2 R).
   Proof. split; apply _. Qed.
   Global Instance: PreOrder R → PreOrder (Forall2 R).
@@ -2768,14 +2768,14 @@ Section bind.
     - by apply contains_app.
     - by rewrite !(assoc_L (++)), (comm (++) (f _)).
     - by apply contains_inserts_l.
-    - etransitivity; eauto.
+    - etrans; eauto.
   Qed.
   Global Instance bind_Permutation: Proper ((≡ₚ) ==> (≡ₚ)) (mbind f).
   Proof.
     induction 1; csimpl; auto.
     - by f_equiv.
     - by rewrite !(assoc_L (++)), (comm (++) (f _)).
-    - etransitivity; eauto.
+    - etrans; eauto.
   Qed.
   Lemma bind_cons x l : (x :: l) ≫= f = f x ++ l ≫= f.
   Proof. done. Qed.
@@ -2998,7 +2998,7 @@ Lemma foldr_permutation {A B} (R : relation B) `{!Equivalence R}
     (f : A → B → B) (b : B) `{!Proper ((=) ==> R ==> R) f}
     (Hf : ∀ a1 a2 b, R (f a1 (f a2 b)) (f a2 (f a1 b))) :
   Proper ((≡ₚ) ==> R) (foldr f b).
-Proof. induction 1; simpl; [done|by f_equiv|apply Hf|etransitivity; eauto]. Qed.
+Proof. induction 1; simpl; [done|by f_equiv|apply Hf|etrans; eauto]. Qed.
 
 (** ** Properties of the [zip_with] and [zip] functions *)
 Section zip_with.
diff --git a/prelude/numbers.v b/prelude/numbers.v
index 7533a75d1c0403087e93b09db93c39adeae50217..215ee4bb8a5ae7337eb7b7cef1c81e7d77f0b683 100644
--- a/prelude/numbers.v
+++ b/prelude/numbers.v
@@ -243,7 +243,7 @@ Proof.
   intros [??] ?.
   destruct (decide (y = 1)); subst; [rewrite Z.quot_1_r; auto |].
   destruct (decide (x = 0)); subst; [rewrite Z.quot_0_l; auto with lia |].
-  split. apply Z.quot_pos; lia. transitivity x; auto. apply Z.quot_lt; lia.
+  split. apply Z.quot_pos; lia. trans x; auto. apply Z.quot_lt; lia.
 Qed.
 
 (* Note that we cannot disable simpl for [Z.of_nat] as that would break
@@ -396,7 +396,7 @@ Lemma Qcplus_pos_pos (x y : Qc) : 0 < x → 0 < y → 0 < x + y.
 Proof. auto using Qcplus_pos_nonneg, Qclt_le_weak. Qed.
 Lemma Qcplus_nonneg_nonneg (x y : Qc) : 0 ≤ x → 0 ≤ y → 0 ≤ x + y.
 Proof.
-  intros. transitivity (x + 0); [by rewrite Qcplus_0_r|].
+  intros. trans (x + 0); [by rewrite Qcplus_0_r|].
   by apply Qcplus_le_mono_l.
 Qed.
 Lemma Qcplus_neg_nonpos (x y : Qc) : x < 0 → y ≤ 0 → x + y < 0.
@@ -410,7 +410,7 @@ Lemma Qcplus_neg_neg (x y : Qc) : x < 0 → y < 0 → x + y < 0.
 Proof. auto using Qcplus_nonpos_neg, Qclt_le_weak. Qed.
 Lemma Qcplus_nonpos_nonpos (x y : Qc) : x ≤ 0 → y ≤ 0 → x + y ≤ 0.
 Proof.
-  intros. transitivity (x + 0); [|by rewrite Qcplus_0_r].
+  intros. trans (x + 0); [|by rewrite Qcplus_0_r].
   by apply Qcplus_le_mono_l.
 Qed.
 Lemma Qcmult_le_mono_nonneg_l x y z : 0 ≤ z → x ≤ y → z * x ≤ z * y.
@@ -436,7 +436,7 @@ Proof.
 Qed.
 Lemma Qcmult_nonneg_nonneg x y : 0 ≤ x → 0 ≤ y → 0 ≤ x * y.
 Proof.
-  intros. transitivity (0 * y); [by rewrite Qcmult_0_l|].
+  intros. trans (0 * y); [by rewrite Qcmult_0_l|].
   by apply Qcmult_le_mono_nonneg_r.
 Qed.
 
diff --git a/prelude/option.v b/prelude/option.v
index ed5cf645db0c41dff17f9843e1b0ce112e330877..b80a955e4d00a763d096b2c8a820c509654f2862 100644
--- a/prelude/option.v
+++ b/prelude/option.v
@@ -96,7 +96,7 @@ Section setoids.
     split.
     - by intros []; constructor.
     - by destruct 1; constructor.
-    - destruct 1; inversion 1; constructor; etransitivity; eauto.
+    - destruct 1; inversion 1; constructor; etrans; eauto.
   Qed.
   Global Instance Some_proper : Proper ((≡) ==> (≡)) (@Some A).
   Proof. by constructor. Qed.
diff --git a/prelude/orders.v b/prelude/orders.v
index 3d74a2b98de74741b62f699edaae1039dd6ad043..423dc320e2e45d11d4904c30629ea6599c9c4b27 100644
--- a/prelude/orders.v
+++ b/prelude/orders.v
@@ -29,13 +29,13 @@ Section orders.
   Proof. by intros [??] <-. Qed.
   Lemma strict_transitive_l `{!Transitive R} X Y Z : X ⊂ Y → Y ⊆ Z → X ⊂ Z.
   Proof.
-    intros [? HXY] ?. split; [by transitivity Y|].
-    contradict HXY. by transitivity Z.
+    intros [? HXY] ?. split; [by trans Y|].
+    contradict HXY. by trans Z.
   Qed.
   Lemma strict_transitive_r `{!Transitive R} X Y Z : X ⊆ Y → Y ⊂ Z → X ⊂ Z.
   Proof.
-    intros ? [? HYZ]. split; [by transitivity Y|].
-    contradict HYZ. by transitivity X.
+    intros ? [? HYZ]. split; [by trans Y|].
+    contradict HYZ. by trans X.
   Qed.
   Global Instance: Irreflexive (strict R).
   Proof. firstorder. Qed.
@@ -79,7 +79,7 @@ Section strict_orders.
   Proof. intros ->. apply (irreflexivity R). Qed.
   Lemma strict_anti_symm `{!StrictOrder R} X Y :
     X ⊂ Y → Y ⊂ X → False.
-  Proof. intros. apply (irreflexivity R X). by transitivity Y. Qed.
+  Proof. intros. apply (irreflexivity R X). by trans Y. Qed.
   Global Instance trichotomyT_dec `{!TrichotomyT R, !StrictOrder R} X Y :
       Decision (X ⊂ Y) :=
     match trichotomyT R X Y with
@@ -101,7 +101,7 @@ Ltac simplify_order := repeat
       assert (x = y) by (by apply (anti_symm R)); clear H1 H2
     | H2 : R y ?z |- _ =>
       unless (R x z) by done;
-      assert (R x z) by (by transitivity y)
+      assert (R x z) by (by trans y)
     end
   end.
 
@@ -319,13 +319,13 @@ Section preorder.
     split.
     - done.
     - by intros ?? [??].
-    - by intros X Y Z [??] [??]; split; transitivity Y.
+    - by intros X Y Z [??] [??]; split; trans Y.
   Qed.
   Global Instance: Proper ((≡) ==> (≡) ==> iff) ((⊆) : relation A).
   Proof.
     unfold equiv, preorder_equiv. intros X1 Y1 ? X2 Y2 ?. split; intro.
-    - transitivity X1. tauto. transitivity X2; tauto.
-    - transitivity Y1. tauto. transitivity Y2; tauto.
+    - trans X1. tauto. trans X2; tauto.
+    - trans Y1. tauto. trans Y2; tauto.
   Qed.
   Lemma subset_spec (X Y : A) : X ⊂ Y ↔ X ⊆ Y ∧ X ≢ Y.
   Proof.
@@ -376,9 +376,9 @@ Section join_semi_lattice.
 
   Hint Resolve subseteq_empty union_subseteq_l union_subseteq_r union_least.
   Lemma union_subseteq_l_transitive X1 X2 Y : X1 ⊆ X2 → X1 ⊆ X2 ∪ Y.
-  Proof. intros. transitivity X2; auto. Qed.
+  Proof. intros. trans X2; auto. Qed.
   Lemma union_subseteq_r_transitive X1 X2 Y : X1 ⊆ X2 → X1 ⊆ Y ∪ X2.
-  Proof. intros. transitivity X2; auto. Qed.
+  Proof. intros. trans X2; auto. Qed.
   Hint Resolve union_subseteq_l_transitive union_subseteq_r_transitive.
   Lemma union_preserving_l X Y1 Y2 : Y1 ⊆ Y2 → X ∪ Y1 ⊆ X ∪ Y2.
   Proof. auto. Qed.
@@ -436,7 +436,7 @@ Section join_semi_lattice.
   Proof.
     split.
     - intros HXY. split; apply equiv_empty;
-        by transitivity (X ∪ Y); [auto | rewrite HXY].
+        by trans (X ∪ Y); [auto | rewrite HXY].
     - intros [HX HY]. by rewrite HX, HY, (left_id _ _).
   Qed.
   Lemma empty_union_list Xs : ⋃ Xs ≡ ∅ ↔ Forall (≡ ∅) Xs.
@@ -502,9 +502,9 @@ Section meet_semi_lattice.
   Hint Resolve intersection_subseteq_l intersection_subseteq_r
     intersection_greatest.
   Lemma intersection_subseteq_l_transitive X1 X2 Y : X1 ⊆ X2 → X1 ∩ Y ⊆ X2.
-  Proof. intros. transitivity X1; auto. Qed.
+  Proof. intros. trans X1; auto. Qed.
   Lemma intersection_subseteq_r_transitive X1 X2 Y : X1 ⊆ X2 → Y ∩ X1 ⊆ X2.
-  Proof. intros. transitivity X1; auto. Qed.
+  Proof. intros. trans X1; auto. Qed.
   Hint Resolve intersection_subseteq_l_transitive
     intersection_subseteq_r_transitive.
   Lemma intersection_preserving_l X Y1 Y2 : Y1 ⊆ Y2 → X ∩ Y1 ⊆ X ∩ Y2.
diff --git a/prelude/pretty.v b/prelude/pretty.v
index e676fe82f7712c9e163e1393502566257d1c478a..61e4a449b502ca598652a54ce4ba152b69ed2c86 100644
--- a/prelude/pretty.v
+++ b/prelude/pretty.v
@@ -49,7 +49,7 @@ Proof.
     intros x; induction (N.lt_wf_0 x) as [x _ IH]; intros s.
     assert (x = 0 ∨ 0 < x)%N as [->|?] by lia; [by rewrite pretty_N_go_0|].
     rewrite pretty_N_go_step by done.
-    etransitivity; [|by eapply IH, N.div_lt]; simpl; lia. }
+    etrans; [|by eapply IH, N.div_lt]; simpl; lia. }
   intros x; induction (N.lt_wf_0 x) as [x _ IH]; intros y s s'.
   assert ((x = 0 ∨ 0 < x) ∧ (y = 0 ∨ 0 < y))%N as [[->|?] [->|?]] by lia;
     rewrite ?pretty_N_go_0, ?pretty_N_go_step, ?(pretty_N_go_step y) by done.
diff --git a/prelude/relations.v b/prelude/relations.v
index bf964b8feb46a84d555cec438c10c87a13e3b46a..55f33d86e74e4f376c560f181e368b2530e4823a 100644
--- a/prelude/relations.v
+++ b/prelude/relations.v
@@ -70,7 +70,7 @@ Section rtc.
   Lemma rtc_once x y : R x y → rtc R x y.
   Proof. eauto. Qed.
   Lemma rtc_r x y z : rtc R x y → R y z → rtc R x z.
-  Proof. intros. etransitivity; eauto. Qed.
+  Proof. intros. etrans; eauto. Qed.
   Lemma rtc_inv x z : rtc R x z → x = z ∨ ∃ y, R x y ∧ rtc R y z.
   Proof. inversion_clear 1; eauto. Qed.
   Lemma rtc_ind_l (P : A → Prop) (z : A)
@@ -152,7 +152,7 @@ Section rtc.
   Global Instance: Transitive (tc R).
   Proof. exact tc_transitive. Qed.
   Lemma tc_r x y z : tc R x y → R y z → tc R x z.
-  Proof. intros. etransitivity; eauto. Qed.
+  Proof. intros. etrans; eauto. Qed.
   Lemma tc_rtc_l x y z : rtc R x y → tc R y z → tc R x z.
   Proof. induction 1; eauto. Qed.
   Lemma tc_rtc_r x y z : tc R x y → rtc R y z → tc R x z.
diff --git a/prelude/streams.v b/prelude/streams.v
index 30959748e8337fc8f2d6f5292187c54c32fc9f77..114b5c79aaf317866ad5d506b827cc700f814a39 100644
--- a/prelude/streams.v
+++ b/prelude/streams.v
@@ -42,7 +42,7 @@ Proof.
   split.
   - now cofix; intros [??]; constructor.
   - now cofix; intros ?? [??]; constructor.
-  - cofix; intros ??? [??] [??]; constructor; etransitivity; eauto.
+  - cofix; intros ??? [??] [??]; constructor; etrans; eauto.
 Qed.
 Global Instance scons_proper x : Proper ((≡) ==> (≡)) (scons x).
 Proof. by constructor. Qed.
diff --git a/prelude/tactics.v b/prelude/tactics.v
index 120bf0fec279b65d81f9707482d47f3e2bb405db..54d6ddccdfc77397e76f5752812800b4c1d1fd4e 100644
--- a/prelude/tactics.v
+++ b/prelude/tactics.v
@@ -54,6 +54,10 @@ Ltac done :=
 Tactic Notation "by" tactic(tac) :=
   tac; done.
 
+(** Aliases for trans and etrans that are easier to type *)
+Tactic Notation "trans" constr(A) := transitivity A.
+Tactic Notation "etrans" := etransitivity.
+
 (** Tactics for splitting conjunctions:
 
 - [split_and] : split the goal if is syntactically of the shape [_ ∧ _]
diff --git a/program_logic/auth.v b/program_logic/auth.v
index f16ac33e6ed82c850e886c44427d7ffed179e5be..fbaae8208e82aaf54cfee250b61da819a784b36b 100644
--- a/program_logic/auth.v
+++ b/program_logic/auth.v
@@ -49,7 +49,7 @@ Section auth.
     { by eapply (own_alloc (Auth (Excl a) a) N). }
     rewrite pvs_frame_l. rewrite -(pvs_mask_weaken N E) //. apply pvs_strip_pvs.
     rewrite sep_exist_l. apply exist_elim=>γ. rewrite -(exist_intro γ).
-    transitivity (▷ auth_inv γ φ ★ auth_own γ a)%I.
+    trans (▷ auth_inv γ φ ★ auth_own γ a)%I.
     { rewrite /auth_inv -(exist_intro a) later_sep.
       rewrite const_equiv // left_id.
       rewrite [(_ ★ ▷ φ _)%I]comm -assoc. apply sep_mono; first done.
diff --git a/program_logic/resources.v b/program_logic/resources.v
index f3d1ed208ec4be04ec1b01c5b30aaf8278bc2f0b..8645e707b774a01cf60fd0fd7815a54dda8fd626 100644
--- a/program_logic/resources.v
+++ b/program_logic/resources.v
@@ -59,7 +59,7 @@ Proof.
   - intros n; split.
     + done.
     + by destruct 1; constructor.
-    + do 2 destruct 1; constructor; etransitivity; eauto.
+    + do 2 destruct 1; constructor; etrans; eauto.
   - by destruct 1; constructor; apply dist_S.
   - intros n c; constructor.
     + apply (conv_compl n (chain_map wld c)).
diff --git a/program_logic/sts.v b/program_logic/sts.v
index ea318637049004461efd2ad5c6328513e00fc883..74010c7092e14a24ea7cb53a31b6cdb4f15dd114 100644
--- a/program_logic/sts.v
+++ b/program_logic/sts.v
@@ -78,7 +78,7 @@ Section sts.
     rewrite pvs_frame_l. rewrite -(pvs_mask_weaken N E) //.
     apply pvs_strip_pvs.
     rewrite sep_exist_l. apply exist_elim=>γ. rewrite -(exist_intro γ).
-    transitivity (▷ sts_inv γ φ ★ sts_own γ s (⊤ ∖ sts.tok s))%I.
+    trans (▷ sts_inv γ φ ★ sts_own γ s (⊤ ∖ sts.tok s))%I.
     { rewrite /sts_inv -(exist_intro s) later_sep.
       rewrite [(_ ★ ▷ φ _)%I]comm -assoc. apply sep_mono_r.
       by rewrite -later_intro -own_op sts_op_auth_frag_up; last set_solver. }
@@ -110,7 +110,7 @@ Section sts.
     rewrite later_sep [(_ ★ ▷φ _)%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.
-    transitivity (|={E}=> own γ (sts_auth s' T'))%I.
+    trans (|={E}=> own γ (sts_auth s' T'))%I.
     { by apply own_update, sts_update_auth. }
     by rewrite -own_op sts_op_auth_frag_up.
   Qed.