proposition: Lemma bindings_Equal: forall [elt: Type] (tab1 tab2: t elt), tab1 == tab2 -> (forall x, InA (@keyb_eq elt) x (bindings tab1) <-> InA (@keyb_eq elt) x (bindings tab2)).
proof: Proof. intros. destruct x as [k y]. split; apply bindings_Equal_imp; intros. rewrite <- (H k0); auto. rewrite (H k0); auto. Qed.
imports: Coq(Bool Equalities Orders OrdersFacts OrdersLists) Coq(Morphisms Permutation SetoidPermutation) MMaps(Utils Comparisons Interface)