proposition: Lemma lookup_kmap_None {A} (m : M1 A) (j : K2) : kmap f m !! j = None ↔ ∀ i, j = f i → m !! i = None.
proof: Proof. setoid_rewrite eq_None_not_Some. rewrite lookup_kmap_is_Some. naive_solver. Qed.
imports: Coq(Permutation) stdpp(options)