proposition: Lemma lookup_kmap_is_Some {A} (m : M1 A) (j : K2) : is_Some (kmap f m !! j) ↔ ∃ i, j = f i ∧ is_Some (m !! i).
proof: Proof. unfold is_Some. setoid_rewrite lookup_kmap_Some. naive_solver. Qed.
imports: Coq(Permutation) stdpp(options)