proposition: Lemma lookup_union_is_Some {A} (m1 m2 : M A) i : is_Some ((m1 ∪ m2) !! i) ↔ is_Some (m1 !! i) ∨ is_Some (m2 !! i).
proof: Proof. rewrite <-!not_eq_None_Some, !lookup_union_None. destruct (m1 !! i); naive_solver. Qed.
imports: Coq(Permutation) stdpp(options)