proposition: Lemma in_bindings k v (m:t elt) : List.In (k,v) (bindings m) -> In k m.
proof: Proof. intros IN. exists v. apply bindings_spec1, In_InA; eauto with *. Qed.
imports: Coq(Bool Arith BinInt FunInd) Coq(Orders OrdersFacts OrdersLists) MMaps(Comparisons Interface OrdList)