proposition: Lemma lookup_kmap_Some {A} (m : M1 A) (j : K2) x : kmap f m !! j = Some x ↔ ∃ i, j = f i ∧ m !! i = Some x.
proof: Proof. assert (∀ x', (j, x) ∈ prod_map f id <$> map_to_list m → (j, x') ∈ prod_map f id <$> map_to_list m → x = x'). { intros x'. rewrite !elem_of_list_fmap. intros [[j' y1] [??]] [[? y2] [??]]; simplify_eq/=. by apply (map_to_list_unique m j'). } unfold kmap. rewrite <-elem_of_list_to_map', elem_of_list_fmap by done. setoid_rewrite elem_of_map_to_list'. split. - intros [[??] [??]]; naive_solver. - intros [? [??]]. eexists (_, _); naive_solver. Qed.
imports: Coq(Permutation) stdpp(options)