proposition: Lemma lookup_preimg_None_1 m x i : map_preimg m !! x = None → m !! i ≠ Some x.
proof: Proof. induction m as [|i' x' m ? IH] using map_ind; [by rewrite lookup_empty|]. rewrite map_preimg_insert by done. destruct (decide (x = x')) as [->|]. - by rewrite lookup_partial_alter. - rewrite lookup_partial_alter_ne, lookup_insert_Some by done. naive_solver. Qed.
imports: Coq(Permutation) stdpp(options)