proposition: Lemma lookup_union_with_Some m1 m2 i z : union_with f m1 m2 !! i = Some z ↔ (m1 !! i = Some z ∧ m2 !! i = None) ∨ (m1 !! i = None ∧ m2 !! i = Some z) ∨ (∃ x y, m1 !! i = Some x ∧ m2 !! i = Some y ∧ f x y = Some z).
proof: Proof. rewrite lookup_union_with. destruct (m1 !! i), (m2 !! i); compute; naive_solver. Qed.
imports: Coq(Permutation) stdpp(options)