proposition: Lemma bindings_Equiv_eqlistA R (m m' : t elt) : Equiv R m m' <-> eqlistA (K.eq * R)%signature (bindings m) (bindings m').
proof: Proof. intros. unfold Equiv. setoid_rewrite bindings_Eqdom_eqlistA. setoid_rewrite <- bindings_spec1. split. - intros (H,H'). induction H; auto. setoid_rewrite InA_cons in H'. constructor; firstorder. destruct x as (x,e), x' as (x',e'). compute. eapply H'; now left. - split. + induction H; auto. constructor; auto. destruct x, x'; apply H. + assert (Hm := bindings_spec2 m); assert (Hm' := bindings_spec2 m'). induction H; simpl; auto. * now setoid_rewrite InA_nil. * inversion_clear Hm; inversion_clear Hm'. intros k e e'. rewrite !InA_cons. destruct x as (x,v), x' as (x',v'). compute in H. destruct H. intros [E|IN] [E'|IN']; try (compute in E; destruct E); try (compute in E'; destruct E'); subst; eauto. { assert (LT : ltk (x',v') (k,e')) by (eapply SortA_InfA_InA with (eqA:=eqke); eauto with * ). compute in LT. order. } { assert (LT : ltk (x,v) (k,e)) by (eapply SortA_InfA_InA with (l:=l)(eqA:=eqke); eauto with *). compute in LT. order. } Qed.
imports: Coq(Bool Equalities Orders OrdersFacts OrdersLists) Coq(Morphisms Permutation SetoidPermutation) MMaps(Utils Comparisons Interface)