proposition: Lemma lookup_preimg_None m x : map_preimg m !! x = None ↔ ∀ i, m !! i ≠ Some x.
proof: Proof. split; [by eauto using lookup_preimg_None_1|]. intros Hm. apply eq_None_not_Some; intros [X ?]. destruct (set_choose_L X) as [i ?]. { intros ->. by eapply lookup_preimg_Some_non_empty. } by eapply (Hm i), lookup_preimg_Some_1. Qed.
imports: Coq(Permutation) stdpp(options)