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