fact: Fixpoint combine (m : t elt) : t elt' -> t oee' := match m with | nil => map (fun e' => (None,Some e')) | (k,e) :: l => fix combine_aux (m':t elt') : list (key * oee') := match m' with | nil => map (fun e => (Some e,None)) m | (k',e') :: l' => match X.compare k k' with | LT _ => (k,(Some e, None))::combine l m' | EQ _ => (k,(Some e, Some e'))::combine l l' | GT _ => (k',(None,Some e'))::combine_aux l' end end end.
imports: FMapInterface