proposition: Lemma bindings_spec1 m x e : InA eqke (x,e) (bindings m) <-> m@x ↦ e.
proof: Proof. unfold bindings. rewrite bindings_aux_mapsto. rewrite InA_nil. intuition. Qed.
imports: Coq(Bool Arith BinInt FunInd) Coq(Orders OrdersFacts OrdersLists) MMaps(Comparisons Interface OrdList)