proposition: Lemma mergeL_in f l l' acc x : (exists v, InA O.eqke (x,v) (mergeL f l l' acc)) -> (exists v, InA O.eqke (x,v) l) \/ (exists v, InA O.eqke (x,v) l') \/ (exists v, InA O.eqke (x,v) acc).
proof: Proof. revert l' acc. induction l as [|(y,e) l IHl]. - simpl. intros l' acc (v,H). right. apply mapoL_mapsto in H. destruct H as [(y & v' & E & IN & _)|H]. + left; exists v'. rewrite InA_alt. exists (y,v'); split; autom. + firstorder. - induction l' as [|(y',e') l' IHl']; intros acc. + intros (v,H). apply mapoL_mapsto in H; simpl in *. destruct H as [(y' & v' & E & [[= <- <-]|IN] & _)|H]. * left. exists e; eautom. * left. exists v'. rewrite InA_cons. right. rewrite InA_alt. exists (y',v'); autom. * firstorder. + rewrite mergeL_eqn. destmatch; [intros EQ H| intros LT H|intros LT H]; apply IHl in H || apply IHl' in H; clear IHl IHl'; firstorder; setoid_rewrite InA_cons; firstorder; destruct f; simpl in *; firstorder; rewrite InA_cons in H; destruct H as [(H,_)|H]; firstorder; compute in H. * left; exists e. now left. * right;left; exists e'. now left. * left; exists e. now left. Qed.
imports: Coq(Bool BinPos Pnat Setoid SetoidList PeanoNat) Coq(Orders OrdersFacts OrdersLists) MMaps(Utils Interface OrdList GenTree)