fact: Definition map2 : t elt -> t elt' -> t elt'' := map2_opt (fun _ d o => f (Some d) o) (map_option (fun _ d => f (Some d) None)) (map_option (fun _ d' => f None (Some d'))).
imports: FunInd FMapInterface FMapList ZArith Int