diff --git a/theories/channel/proto_channel.v b/theories/channel/proto_channel.v
index 18501ad8bf2bc8348c2e0cf96ffa2b87e4b297c8..b2e01fa867f6b25f02d3eb2f665504d58d1c5020 100644
--- a/theories/channel/proto_channel.v
+++ b/theories/channel/proto_channel.v
@@ -803,3 +803,17 @@ Section proto.
     iIntros "!>" (b) "Hc HP". iApply "HΨ". iFrame.
   Qed.
 End proto.
+
+Ltac f_proto_contractive :=
+  match goal with
+  | _ => apply iProto_branch_contractive
+  | _ => apply iProto_message_contractive; simpl; intros; [reflexivity|..]
+  | H : _ ≡{?n}≡ _ |- _ ≡{?n'}≡ _ => apply (dist_le n); [apply H|lia]
+  end;
+  try match goal with
+  | |- @dist_later ?A _ ?n ?x ?y =>
+         destruct n as [|n]; simpl in *; [exact Logic.I|change (@dist A _ n x y)]
+  end.
+
+Ltac solve_proto_contractive :=
+  solve_proper_core ltac:(fun _ => first [f_contractive | f_proto_contractive | f_equiv]).
diff --git a/theories/examples/list_sort_elem.v b/theories/examples/list_sort_elem.v
index ca6ddf819bafc4c38f290ce39c942f8bb1845e7e..3967fd5c244f9b0b87cf6283ca6e0bdd44b9dc9b 100644
--- a/theories/examples/list_sort_elem.v
+++ b/theories/examples/list_sort_elem.v
@@ -57,10 +57,7 @@ Section list_sort_elem.
      <&{⌜ ys ≡ₚ xs ⌝}> END)%proto.
 
   Instance tail_protocol_aux_contractive xs : Contractive (tail_protocol_aux xs).
-  Proof.
-    intros n p p' Hp ys. apply iProto_branch_ne=> //=.
-    apply iProto_message_contractive=> x //=. destruct n as [|n]=> //=.
-  Qed.
+  Proof. solve_proto_contractive. Qed.
   Definition tail_protocol (xs : list (A * val)) : list (A * val) → iProto Σ :=
     fixpoint (tail_protocol_aux xs).
   Global Instance tail_protocol_unfold xs ys :
@@ -73,10 +70,7 @@ Section list_sort_elem.
      <+> tail_protocol xs [])%proto.
 
   Instance head_protocol_aux_contractive : Contractive head_protocol_aux.
-  Proof.
-    intros n p p' Hp xs. apply iProto_branch_ne=> //=.
-    apply iProto_message_contractive=> //= x. destruct n as [|n]=> //=.
-  Qed.
+  Proof. solve_proto_contractive. Qed.
 
   Definition head_protocol : list (A * val) → iProto Σ := fixpoint head_protocol_aux.
   Global Instance head_protocol_unfold xs :
diff --git a/theories/examples/loop_sort.v b/theories/examples/loop_sort.v
index 4c6dc44b1f950a2926a9af98c4192f773f12fcf2..ff403fb696d2acc95bde6b4fcb1a7b3db229f6ea 100644
--- a/theories/examples/loop_sort.v
+++ b/theories/examples/loop_sort.v
@@ -20,10 +20,7 @@ Section loop_sort.
     ((sort_protocol <++> rec) <+> ((<?> c, MSG c {{ c ↣ rec @ N }}; rec) <+> END))%proto.
 
   Instance loop_sort_protocol_aux_contractive : Contractive loop_sort_protocol_aux.
-  Proof.
-    intros n p p' Hp. rewrite /loop_sort_protocol_aux.
-    f_contractive; f_equiv=> //. apply iProto_message_ne=> c /=; by repeat f_equiv.
-  Qed.
+  Proof. solve_proto_contractive. Qed.
   Definition loop_sort_protocol : iProto Σ := fixpoint loop_sort_protocol_aux.
   Global Instance loop_sort_protocol_unfold :
     ProtoUnfold loop_sort_protocol (loop_sort_protocol_aux loop_sort_protocol).