proposition: Lemma in_bindings_iff' m x e : In x m <-> InA eqk (x,e) (bindings m).
proof: Proof. rewrite in_bindings_iff. split. - intros (e',H). eapply InA_eqA; eauto with *. now compute. - intros H. now exists e. Qed.
imports: Coq(Bool Equalities Orders OrdersFacts OrdersLists) Coq(Morphisms Permutation SetoidPermutation) MMaps(Utils Comparisons Interface)