proposition: Lemma map_agree_kmap {A} (m1 m2 : M1 A) : map_agree (kmap f m1) (kmap f m2) ↔ map_agree m1 m2.
proof: Proof. rewrite !map_agree_spec. setoid_rewrite lookup_kmap_Some. naive_solver. Qed.
imports: Coq(Permutation) stdpp(options)