proposition: Lemma map_fmap_singleton_inv {A B} (f : A → B) (m : M A) i y : f <$> m = {[i := y]} → ∃ x, y = f x ∧ m = {[ i := x ]}.
proof: Proof. intros Hm. pose proof (f_equal (.!! i) Hm) as Hmi. rewrite lookup_fmap, lookup_singleton, fmap_Some in Hmi. destruct Hmi as (x&?&->). exists x. split; [done|]. apply map_eq; intros j. destruct (decide (i = j)) as[->|?]. - by rewrite lookup_singleton. - rewrite lookup_singleton_ne by done. apply (fmap_None f). by rewrite <-lookup_fmap, Hm, lookup_singleton_ne. Qed.
imports: Coq(Permutation) stdpp(options)