proposition: Lemma map_Exists_insert_2_2 m i x : m !! i = None → map_Exists P m → map_Exists P (<[i:=x]>m).
proof: Proof. intros Hm [j[y[??]]]. exists j, y. by rewrite lookup_insert_ne by congruence. Qed.
imports: Coq(Permutation) stdpp(options)