proposition: Lemma lookup_union_Some_inv_r {A} (m1 m2 : M A) i x : (m1 ∪ m2) !! i = Some x → m1 !! i = None → m2 !! i = Some x.
proof: Proof. rewrite lookup_union_Some_raw. naive_solver. Qed.
imports: Coq(Permutation) stdpp(options)