proposition: Lemma natmap_lookup_merge_raw {A B C} (f : option A → option B → option C) l1 l2 i : mjoin (natmap_merge_raw f l1 l2 !! i) = diag_None f (mjoin (l1 !! i)) (mjoin (l2 !! i)).
proof: Proof. intros. revert i l2. induction l1; intros [|?] [|??]; simpl; autorewrite with natmap; auto; match goal with |- context [?o ≫= _] => by destruct o end. Qed.
imports: stdpp(fin_maps mapset) stdpp(options)