proposition: Lemma bindings_aux_mapsto m acc x e : InA eqke (x,e) (bindings_aux acc m) <-> m@x ↦ e \/ InA eqke (x,e) acc.
proof: Proof. revert acc. induction m as [ | h l Hl y e' r Hr ]; intros acc; simpl; auto. - intuition_m. - rewrite Hl, InA_cons, Hr. redk. intuition_m. subst; autom. Qed.
imports: Coq(Bool Arith BinInt FunInd) Coq(Orders OrdersFacts OrdersLists) MMaps(Comparisons Interface OrdList)