proposition: Lemma combine_Inf : forall m m' (x:key)(e:elt)(e':elt')(e'':oee'), Inf (x,e) m -> Inf (x,e') m' -> Inf (x,e'') (combine m m').
proof: Proof. induction m. - intros. simpl. eapply map_Inf; eauto. - induction m'; intros. + destruct a. replace (combine ((t0, e0) :: m) nil) with (map (fun e => (Some e,None (A:=elt'))) ((t0,e0)::m)); auto. eapply map_Inf; eauto. + simpl. destruct a as (k,e0); destruct a0 as (k',e0'). elim X.compare_spec. * inversion_clear H; auto. * inversion_clear H; auto. * inversion_clear H0; auto. Qed.
imports: Coq(OrdersFacts OrdersLists)