From fa8a02f29226fec40506d48d0294b917b3078988 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sun, 24 Feb 2019 13:13:43 +0100
Subject: [PATCH] Permutation Proper instance for `omap` on lists.

---
 theories/list.v | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/theories/list.v b/theories/list.v
index eb19fa71..0bd8b49d 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).
 
-- 
GitLab