proposition: Lemma map_fmap_equiv_ext `{Equiv 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 i; rewrite !lookup_fmap. destruct (m !! i) eqn:?; constructor; eauto. Qed.
imports: Coq(Permutation) stdpp(options)