proposition: Lemma map_singleton_equiv_eq m i x : m ≡ {[i:=x]} ↔ ∃ x', m = {[i:=x']} ∧ x' ≡ x.
proof: Proof. rewrite <-!insert_empty, insert_equiv_eq. setoid_rewrite map_empty_equiv_eq. naive_solver. Qed.
imports: Coq(Permutation) stdpp(options)