proposition: Lemma ApartL_ltk_l A B B' (lA : klist A) (kb:key*B) (kb':key*B') : [kb] < lA -> kb'#1 < kb#1 -> [kb'] < lA.
proof: Proof. intros AP LT (k,b') (k',a) [<-|[ ]] Hy; simpl. rewrite LT. apply (AP kb (k',a)); simpl; auto. Qed.
imports: Coq(Bool BinPos Pnat Setoid SetoidList PeanoNat) Coq(Orders OrdersFacts OrdersLists) MMaps(Utils Interface OrdList GenTree)