proposition: Lemma map2_0 : forall m (Hm:NoDupA (@eqk elt) m) m' (Hm':NoDupA (@eqk elt') m')(x:key), find x (map2 m m') = at_least_one_then_f (find x m) (find x m').
proof: Proof. intros. unfold map2. assert (H:=combine_1 Hm Hm' x). assert (H2:=combine_NoDup Hm Hm'). set (f':= fun p : oee' => f (fst p) (snd p)). set (m0 := combine m m') in *; clearbody m0. set (o:=find x m) in *; clearbody o. set (o':=find x m') in *; clearbody o'. clear Hm Hm' m m'. generalize H; clear H. match goal with |- ?m=?n -> ?p=?q => assert ((m=n->p=q)/\(m=None -> p=None)); [|intuition] end. induction m0; simpl in *; intuition. - destruct o; destruct o'; simpl in *; try discriminate; auto. - destruct a as (k,(oo,oo')); simpl in *. inversion_clear H2. destruct (X.eq_dec x k) as [|Hneq]; simpl in *. + assert (at_least_one_then_f o o' = f oo oo'). * destruct o; destruct o'; simpl in *; inversion_clear H; auto. * rewrite H2. unfold f'; simpl. destruct (f oo oo'); simpl. -- destruct (X.eq_dec x k) as [|Hneq]; try contradict Hneq; auto. -- destruct (IHm0 H1) as (_,H4); apply H4; auto. case_eq (find x m0); intros; auto. elim H0. apply InA_eqk with (x,p); auto. apply InA_eqke_eqk. exact (find_2 H3). + unfold f'; simpl. destruct (f oo oo'); simpl. * destruct (X.eq_dec x k); [ contradict Hneq; auto | auto]. destruct (IHm0 H1) as (H3,_); apply H3; auto. * destruct (IHm0 H1) as (H3,_); apply H3; auto. - destruct a as (k,(oo,oo')). simpl. inversion_clear H2. destruct (X.eq_dec x k) as [|Hneq]. + discriminate. + unfold f'; simpl. destruct (f oo oo'); simpl. * destruct (X.eq_dec x k); [ contradict Hneq; auto | auto]. destruct (IHm0 H1) as (_,H4); apply H4; auto. * destruct (IHm0 H1) as (_,H4); apply H4; auto. Qed.
imports: FMapInterface