proposition: Lemma combine_1 : forall m (Hm:NoDupA (@eqk elt) m) m' (Hm':NoDupA (@eqk elt') m')(x:key), find x (combine m m') = at_least_one (find x m) (find x m').
proof: Proof. unfold combine. intros. generalize (combine_r_1 Hm Hm' x). generalize (combine_l_1 Hm Hm' x). assert (NoDupA (eqk (elt:=oee')) (combine_l m m')). { unfold combine_l; apply mapi_NoDup; auto. } assert (NoDupA (eqk (elt:=oee')) (combine_r m m')). { unfold combine_r; apply mapi_NoDup; auto. } set (l := combine_l m m') in *; clearbody l. set (r := combine_r m m') in *; clearbody r. set (o := find x m); clearbody o. set (o' := find x m'); clearbody o'. clear Hm' Hm m m'. induction l. - destruct o; destruct o'; simpl; intros; discriminate || auto. - destruct a; simpl in *; intros. destruct (X.eq_dec x t0); simpl in *. + unfold at_least_left in H1. destruct o; simpl in *; try discriminate. inversion H1; subst. apply add_eq; auto. inversion_clear H; auto. + inversion_clear H. rewrite <- IHl; auto. apply add_not_eq; auto. Qed.
imports: FMapInterface