proposition: Lemma omap_ext {A B} (f1 f2 : A → option B) (m : M A) : (∀ i x, m !! i = Some x → f1 x = f2 x) → omap f1 m = omap f2 m.
proof: Proof. intros Hi; apply map_eq; intros i; rewrite !lookup_omap. by destruct (m !! i) eqn:?; simpl; erewrite ?Hi by eauto. Qed.
imports: Coq(Permutation) stdpp(options)