proposition: Lemma bindings_sort (m:t elt) : sort O.ltk (bindings m) <-> Ok m.
proof: Proof. split; auto using bindings_spec2. induction m as [|c l IHl x v r IHr]. - unfold bindings. simpl. constructor. - rewrite bindings_node; simpl. rewrite sort_app_key, sort_cons_key, (@ApartL_consr _ elt). rewrite <- bindings_above, <- bindings_below. intuition auto; ok. Qed.
imports: Coq(Bool BinPos Pnat Setoid SetoidList PeanoNat) Coq(Orders OrdersFacts OrdersLists) MMaps(Utils Interface OrdList GenTree)