proposition: Lemma equal_2 : forall (A:Type)(m m':t A)(cmp:A->A->bool), equal cmp m m' = true -> Equivb cmp m m'.
proof: Proof. induction m. simpl. split; intros. split. destruct 1; red in H0; destruct k; discriminate. rewrite is_empty_spec in H. intros (e,H'). red in H'. now rewrite H in H'. red in H0; destruct k; discriminate. destruct m'. simpl. destruct o; intros; try discriminate. destruct (andb_prop _ _ H); clear H. split; intros. split; unfold In, MapsTo; destruct 1. destruct k; simpl in *; try discriminate. rewrite is_empty_spec in H1. now rewrite H1 in H. rewrite is_empty_spec in H0. now rewrite H0 in H. destruct k; simpl in *; discriminate. unfold In, MapsTo; destruct k; simpl in *; discriminate. destruct o; destruct o0; simpl; intros; try discriminate. destruct (andb_prop _ _ H); clear H. destruct (andb_prop _ _ H0); clear H0. destruct (IHm1 _ _ H2); clear H2 IHm1. destruct (IHm2 _ _ H1); clear H1 IHm2. unfold Eqdom in *. split; intros. red. destruct k; unfold In, MapsTo in *; simpl; auto. split; eauto. destruct k; unfold In, MapsTo in *; simpl in *. eapply H4; eauto. eapply H3; eauto. congruence. destruct (andb_prop _ _ H); clear H. destruct (IHm1 _ _ H0); clear H0 IHm1. destruct (IHm2 _ _ H1); clear H1 IHm2. unfold Eqdom in *. split; intros. red. destruct k; unfold In, MapsTo in *; simpl; auto. split; eauto. destruct k; unfold In, MapsTo in *; simpl in *. eapply H3; eauto. eapply H2; eauto. try discriminate. Qed.
imports: Coq(Bool PeanoNat BinPos Orders OrdersEx OrdersLists) MMaps(Utils Comparisons Interface)