proposition: Lemma lookup_singleton_Some {A} i j (x y : A) : ({[i := x]} : M A) !! j = Some y ↔ i = j ∧ x = y.
proof: Proof. rewrite <-insert_empty,lookup_insert_Some, lookup_empty; intuition congruence. Qed.
imports: Coq(Permutation) stdpp(options)