proposition: Lemma map_choose {A} (m : M A) : m ≠ ∅ → ∃ i x, m !! i = Some x.
proof: Proof. rewrite <-map_to_list_empty_iff. intros Hemp. destruct (map_to_list m) as [|[i x] l] eqn:Hm; [done|]. exists i, x. rewrite <-elem_of_map_to_list, Hm. by left. Qed.
imports: Coq(Permutation) stdpp(options)