diff --git a/CHANGELOG.md b/CHANGELOG.md
index 77a7838a513a2698f152d4962fcad0529db8149e..a28b5914352ab7b5a58f60f80224136faa7267f9 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -95,6 +95,8 @@ API-breaking change is listed.
     `bsteps_rtc` → `rtc_bsteps_2`.
   - Add lemmas that relate `rtc`, `tc`, `nsteps`, and `bsteps` to path
     representations as lists.
+- Remove explicit equality from cross split lemmas so that they become easier
+  to use in forward-style proofs.
 
 The following `sed` script should perform most of the renaming
 (on macOS, replace `sed` by `gsed`, installed via e.g. `brew install gnu-sed`):
diff --git a/theories/fin_maps.v b/theories/fin_maps.v
index b5a020c2b1cbcebec0a4e689ef4da57f9aa98910..8167e863e396cdeb3026eed8d99307f784cf120a 100644
--- a/theories/fin_maps.v
+++ b/theories/fin_maps.v
@@ -2191,26 +2191,26 @@ Proof.
   destruct (m1 !! i), (m2 !! i); simpl; repeat (destruct (f _)); naive_solver.
 Qed.
 
-Lemma map_cross_split {A} (m ma mb mc md : M A) :
+Lemma map_cross_split {A} (ma mb mc md : M A) :
   ma ##ₘ mb → mc ##ₘ md →
-  ma ∪ mb = m → mc ∪ md = m →
+  ma ∪ mb = mc ∪ md →
   ∃ mac mad mbc mbd,
     mac ##ₘ mad ∧ mbc ##ₘ mbd ∧
     mac ##ₘ mbc ∧ mad ##ₘ mbd ∧
     mac ∪ mad = ma ∧ mbc ∪ mbd = mb ∧ mac ∪ mbc = mc ∧ mad ∪ mbd = md.
 Proof.
-  intros Hab_disj Hcd_disj Hab Hcd.
+  intros Hab_disj Hcd_disj Hab.
   exists (filter (λ kx, is_Some (mc !! kx.1)) ma),
     (filter (λ kx, ¬is_Some (mc !! kx.1)) ma),
     (filter (λ kx, is_Some (mc !! kx.1)) mb),
     (filter (λ kx, ¬is_Some (mc !! kx.1)) mb).
   split_and!; [auto using map_disjoint_filter_complement, map_disjoint_filter,
     map_filter_union_complement..| |].
-  - rewrite <-map_filter_union, Hab, <-Hcd by done.
+  - rewrite <-map_filter_union, Hab by done.
     apply map_eq; intros k. apply option_eq; intros x.
     rewrite map_filter_lookup_Some, lookup_union_Some, <-not_eq_None_Some by done.
     rewrite map_disjoint_alt in Hcd_disj; naive_solver.
-  - rewrite <-map_filter_union, Hab, <-Hcd by done.
+  - rewrite <-map_filter_union, Hab by done.
     apply map_eq; intros k. apply option_eq; intros x.
     rewrite map_filter_lookup_Some, lookup_union_Some, <-not_eq_None_Some by done.
     rewrite map_disjoint_alt in Hcd_disj; naive_solver.
diff --git a/theories/list.v b/theories/list.v
index 6087a9ca6b4548017d46e7eadbd5e70a6b83430e..0e220fd345fecdcf652ff70d99c144da4043c769 100644
--- a/theories/list.v
+++ b/theories/list.v
@@ -1833,18 +1833,17 @@ Lemma Permutation_cons_inv_l l k x :
   x :: l ≡ₚ k → ∃ k1 k2, k = k1 ++ x :: k2 ∧ l ≡ₚ k1 ++ k2.
 Proof. by intros ?%(symmetry_iff (≡ₚ))%Permutation_cons_inv_r. Qed.
 
-Lemma Permutation_cross_split l la lb lc ld :
-  la ++ lb ≡ₚ l →
-  lc ++ ld ≡ₚ l →
+Lemma Permutation_cross_split (la lb lc ld : list A) :
+  la ++ lb ≡ₚ lc ++ ld →
   ∃ lac lad lbc lbd,
     lac ++ lad ≡ₚ la ∧ lbc ++ lbd ≡ₚ lb ∧ lac ++ lbc ≡ₚ lc ∧ lad ++ lbd ≡ₚ ld.
 Proof.
-  intros <-. revert lc ld.
+  revert lc ld.
   induction la as [|x la IH]; simpl; intros lc ld Hperm.
   { exists [], [], lc, ld. by rewrite !(right_id_L [] (++)). }
   assert (x ∈ lc ++ ld)
     as [[lc' Hlc]%elem_of_Permutation|[ld' Hld]%elem_of_Permutation]%elem_of_app.
-  { rewrite Hperm, elem_of_cons. auto. }
+  { rewrite <-Hperm, elem_of_cons. auto. }
   - rewrite Hlc in Hperm. simpl in Hperm. apply (inj (x ::.)) in Hperm.
     apply IH in Hperm as (lac&lad&lbc&lbd&Ha&Hb&Hc&Hd).
     exists (x :: lac), lad, lbc, lbd; simpl. by rewrite Ha, Hb, Hc, Hd.
diff --git a/theories/numbers.v b/theories/numbers.v
index 452bd8339d9f758577e616a340df2b6026c8535d..9600f0fc46d6493dc07613f450e13acb954beb22 100644
--- a/theories/numbers.v
+++ b/theories/numbers.v
@@ -1118,11 +1118,11 @@ Proof.
   exists qmin. split; eapply Qp_lt_sum; eauto.
 Qed.
 
-Lemma Qp_cross_split p a b c d :
-  a + b = p → c + d = p →
+Lemma Qp_cross_split a b c d :
+  a + b = c + d →
   ∃ ac ad bc bd, ac + ad = a ∧ bc + bd = b ∧ ac + bc = c ∧ ad + bd = d.
 Proof.
-  intros H <-. revert a b c d H. cut (∀ a b c d : Qp,
+  intros H. revert a b c d H. cut (∀ a b c d : Qp,
     a < c → a + b = c + d →
     ∃ ac ad bc bd, ac + ad = a ∧ bc + bd = b ∧ ac + bc = c ∧ ad + bd = d)%Qp.
   { intros help a b c d Habcd.