fact: Definition natmap_merge_raw {A B C} (f : option A → option B → option C) : natmap_raw A → natmap_raw B → natmap_raw C := fix go l1 l2 := match l1, l2 with | [], l2 => natmap_omap_raw (f None ∘ Some) l2 | l1, [] => natmap_omap_raw (flip f None ∘ Some) l1 | o1 :: l1, o2 :: l2 => natmap_cons_canon (diag_None f o1 o2) (go l1 l2) end.
imports: stdpp(fin_maps mapset) stdpp(options)