proposition: Lemma findL_app {elt} x (l l' : klist elt) : findL x (l++l') = oelse (findL x l) (findL x l').
proof: Proof. induction l as [|(y,v) l IH]; simpl; auto. rewrite IH. destmatch; auto. Qed.
imports: Coq(Bool BinPos Pnat Setoid SetoidList PeanoNat) Coq(Orders OrdersFacts OrdersLists) MMaps(Utils Interface OrdList GenTree)