proposition: Lemma in_fst_bindings_iff m x : In x m <-> InA K.eq x (List.map fst (bindings m)).
proof: Proof. rewrite InA_alt. setoid_rewrite in_map_iff. rewrite in_bindings_iff. setoid_rewrite InA_alt. firstorder. subst. exists (snd x1). firstorder. Qed.
imports: Coq(Bool Equalities Orders OrdersFacts OrdersLists) Coq(Morphisms Permutation SetoidPermutation) MMaps(Utils Comparisons Interface)