diff --git a/theories/list.v b/theories/list.v
index eb19fa71481cdd448c9f3799f3c49fe882790077..0bd8b49da77e1bf28e9502eab336a4f46d3f1f7c 100644
--- a/theories/list.v
+++ b/theories/list.v
@@ -3133,6 +3133,10 @@ Proof.
   - apply IH. intros. eapply Hunique; rewrite ?elem_of_cons; eauto.
 Qed.
 
+Global Instance omap_Permutation {A B} (f : A → option B) :
+  Proper ((≡ₚ) ==> (≡ₚ)) (omap f).
+Proof. induction 1; simpl; repeat case_match; econstructor; eauto. Qed.
+
 Section bind.
   Context {A B : Type} (f : A → list B).