proposition: Lemma ApartL_eqk_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 E (k,b') (k',a) [<-|[ ]] Hy; simpl. rewrite <-E. 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)