proposition: Lemma ApartL_consl ka lA lB : (ka::lA) < lB <-> [ka] < lB /\ lA < lB.
proof: Proof. apply (ApartL_appl [ka]). Qed.
imports: Coq(Bool BinPos Pnat Setoid SetoidList PeanoNat) Coq(Orders OrdersFacts OrdersLists) MMaps(Utils Interface OrdList GenTree)