proposition: Lemma bindings_Add_Below : forall m m' x e, Below x m -> Add x e m m' -> eqlistA eqke (bindings m') ((x,e)::bindings m).
proof: Proof. intros. apply sort_equivlistA_eqlistA; auto with *. change (sort ltk (((x,e)::nil) ++ bindings m)). apply (@SortA_app _ eqke); auto with *. intros. inversion_clear H1. destruct y; destruct x0. rewrite <- bindings_mapsto_iff in H2. destruct H3; klean. rewrite H1. apply H; firstorder. inversion H3. red; intros a; destruct a. rewrite InA_cons, <- 2 bindings_mapsto_iff, find_mapsto_iff, (H0 t0), <- find_mapsto_iff, add_mapsto_iff by (auto with * ). change (eqke (t0,e0) (x,e)) with (K.eq t0 x /\ e0 = e). intuition (auto with map). destruct (K.eq_dec x t0) as [Heq|Hneq]; auto. exfalso. assert (In t0 m) by (exists e0; auto). generalize (H t0 H1). F.order. Qed.
imports: Coq(Bool Equalities Orders OrdersFacts OrdersLists) Coq(Morphisms Permutation SetoidPermutation) MMaps(Utils Comparisons Interface)