proposition: Lemma map_img_singleton_inv m i x : map_img m ≡ {[ x ]} → m !! i = None ∨ m !! i = Some x.
proof: Proof. intros Hm. destruct (m !! i) eqn:Hmk; [|by auto]. apply elem_of_map_img_2 in Hmk. set_solver. Qed.
imports: Coq(Permutation) stdpp(options)