proposition: Lemma lookup_preimg_Some m x X : map_preimg m !! x = Some X ↔ X ≠ ∅ ∧ ∀ i, i ∈ X ↔ m !! i = Some x.
proof: Proof. split. - intros HxX. split; [intros ->; by eapply lookup_preimg_Some_non_empty|]. intros j. by apply lookup_preimg_Some_1. - intros [HXne HX]. destruct (map_preimg m !! x) as [X'|] eqn:HX'. + f_equal; apply set_eq; intros i. rewrite HX. by apply lookup_preimg_Some_1. + apply set_choose_L in HXne as [j ?]. apply (lookup_preimg_None_1 _ _ j) in HX'. naive_solver. Qed.
imports: Coq(Permutation) stdpp(options)