proposition: Lemma ApartL_appl lA lA' lB : lA++lA' < lB <-> lA < lB /\ lA' < lB.
proof: Proof. unfold "<", lt_klist. setoid_rewrite in_app_iff; firstorder. Qed.
imports: Coq(Bool BinPos Pnat Setoid SetoidList PeanoNat) Coq(Orders OrdersFacts OrdersLists) MMaps(Utils Interface OrdList GenTree)