proposition: Lemma lookup_intersection_Some {A} (m1 m2 : M A) i x : (m1 ∩ m2) !! i = Some x ↔ m1 !! i = Some x ∧ is_Some (m2 !! i).
proof: Proof. unfold intersection, map_intersection. rewrite lookup_intersection_with. destruct (m1 !! i), (m2 !! i); compute; naive_solver. Qed.
imports: Coq(Permutation) stdpp(options)