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