proposition: Lemma map_non_empty_singleton {A} i (x : A) : {[i := x]} ≠@{M A} ∅.
proof: Proof. intros Hix. apply (f_equal (.!! i)) in Hix. by rewrite lookup_empty, lookup_singleton in Hix. Qed.
imports: Coq(Permutation) stdpp(options)