proposition: Lemma lookup_union_Some {A} (m1 m2 : M A) i x : m1 ##ₘ m2 → (m1 ∪ m2) !! i = Some x ↔ m1 !! i = Some x ∨ m2 !! i = Some x.
proof: Proof. intros Hdisjoint. rewrite lookup_union_Some_raw. intuition eauto using map_disjoint_Some_r. Qed.
imports: Coq(Permutation) stdpp(options)