proposition: Lemma combine_lelistA : forall m m' (x:key)(e:elt)(e':elt')(e'':oee'), lelistA (@ltk elt) (x,e) m -> lelistA (@ltk elt') (x,e') m' -> lelistA (@ltk oee') (x,e'') (combine m m').
proof: Proof. induction m. - intros. simpl. exact (map_lelistA _ _ H0). - induction m'. + intros. destruct a. replace (combine ((t0, e0) :: m) nil) with (map (fun e => (Some e,None (A:=elt'))) ((t0,e0)::m)); auto. exact (map_lelistA _ _ H). + intros. simpl. destruct a as (k,e0); destruct a0 as (k',e0'). destruct (X.compare k k'). * inversion_clear H; auto. * inversion_clear H; auto. * inversion_clear H0; auto. Qed.
imports: FMapInterface