proposition: Lemma lookup_difference_is_Some {A} (m1 m2 : M A) i : is_Some ((m1 ∖ m2) !! i) ↔ is_Some (m1 !! i) ∧ m2 !! i = None.
proof: Proof. unfold is_Some. setoid_rewrite lookup_difference_Some. naive_solver. Qed.
imports: Coq(Permutation) stdpp(options)