proposition: Lemma bindings_Equal_imp: forall [elt: Type] (tab1 tab2: t elt), (forall k y, find k tab1 = Some y -> find k tab2 = Some y) -> (forall x, InA (@keyb_eq elt) x (bindings tab1) -> InA (@keyb_eq elt) x (bindings tab2)).
proof: Proof. intros. destruct x as [k y]. specialize (H k). rewrite !bindings_o in H. pose proof bindings_3w tab1. pose proof bindings_3w tab2. set (al := bindings tab1) in *. clearbody al. set (bl := bindings tab2) in *. clearbody bl. revert bl H H1 H2 y H0; induction al as [ | [? ?]]; simpl; intros. - inversion H0. - inversion H1; clear H1; subst. inversion H0; clear H0; subst. + destruct H3; simpl in *. subst. rewrite (proj2 (eqb_eq _ _)) in H by auto. specialize (H _ (Logic.eq_refl _)). clear - H. induction bl as [ | [? ? ]]. inversion H. simpl in *. destruct (eqb k k0) eqn:?H. inversion H; clear H; subst. left. split; auto. apply eqb_eq; auto. right. auto. + destruct (eqb k k0) eqn:?H. * apply IHal; auto. intros. apply eqb_eq in H0. contradiction H5. clear - H0 H1. induction al as [ | [? ?]]. inversion H1. simpl in *. destruct (eqb k k1) eqn:?H. inversion H1; clear H1; subst. left; hnf. simpl. transitivity k. symmetry; auto. apply eqb_eq; auto. right; auto. * apply IHal; auto; intros. Qed.
imports: Coq(Bool Equalities Orders OrdersFacts OrdersLists) Coq(Morphisms Permutation SetoidPermutation) MMaps(Utils Comparisons Interface)