proposition: Lemma in_bindings_iff m x : In x m <-> exists e, InA eqk (x,e) (bindings m).
proof: Proof. rewrite bindings_in_iff. split. - intros (e,H). apply InA_eqke_eqk with (k':=x) (e':=e) in H. firstorder. reflexivity. - intros (e,H). eapply InA_eqk_eqke; eauto. Qed.
imports: Coq(Bool Equalities Orders OrdersFacts OrdersLists) Coq(Morphisms Permutation SetoidPermutation) MMaps(Utils Comparisons Interface)