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