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. * destruct 1; elim (is_empty_2 H H0). + 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. ++ destruct (is_empty_2 H1 (find_2 _ _ H)). ++ destruct (is_empty_2 H0 (find_2 _ _ 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. split; intros. -- 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. split; intros. -- 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: Bool OrderedType ZArith OrderedType OrderedTypeEx FMapInterface