proposition: Lemma lookup_preimg_Some_non_empty m x : map_preimg m !! x ≠ Some ∅.
proof: Proof. induction m as [|i x' m ? IH] using map_ind. { by rewrite map_preimg_empty, lookup_empty. } rewrite map_preimg_insert by done. destruct (decide (x = x')) as [->|]. - rewrite lookup_partial_alter. intros [=]. set_solver. - rewrite lookup_partial_alter_ne by done. set_solver. Qed.
imports: Coq(Permutation) stdpp(options)