proposition: Lemma lookup_preimg_Some_1 m X x i : map_preimg m !! x = Some X → i ∈ X ↔ m !! i = Some x.
proof: Proof. revert X. induction m as [|i' x' m ? IH] using map_ind; intros X. { by rewrite map_preimg_empty, lookup_empty. } rewrite map_preimg_insert by done. destruct (decide (x = x')) as [->|]. - rewrite lookup_partial_alter. intros [= <-]. rewrite elem_of_union, elem_of_singleton, lookup_insert_Some. destruct (map_preimg m !! x') as [X'|] eqn:Hx'; simpl. + rewrite IH by done. naive_solver. + apply (lookup_preimg_None_1 _ _ i) in Hx'. set_solver. - rewrite lookup_partial_alter_ne, lookup_insert_Some by done. naive_solver. Qed.
imports: Coq(Permutation) stdpp(options)