proposition: Lemma split_in_l0 m x y : y ∈ (split x m)#l -> y ∈ m.
proof: Proof. functional induction (split x m); cleansplit; rewrite ?join_in; intuition_in. Qed.
imports: Coq(Bool PeanoNat BinInt FunInd Int) Coq(Orders OrdersFacts OrdersLists) MMaps(Utils Interface OrdList GenTree)