proposition: Lemma equal_1 : forall (A:Type)(m m':t A)(cmp:A->A->bool), Equivb cmp m m' -> equal cmp m m' = true.
proof: Proof. induction m. - destruct 1. simpl. apply is_empty_1. red; red; intros. assert (In a (Leaf A)). + rewrite H. exists e; auto. + destruct H2; red in H2. destruct a; simpl in *; discriminate. - destruct m'. + destruct 1. simpl. destruct o. * assert (In xH (Leaf A)). { rewrite <- H. exists a; red; auto. } destruct H1; red in H1; simpl in H1; discriminate. * apply andb_true_intro; split; apply is_empty_1; red; red; intros. -- assert (In (xO a) (Leaf A)). { rewrite <- H. exists e; auto. } destruct H2; red in H2; simpl in H2; discriminate. -- assert (In (xI a) (Leaf A)). { rewrite <- H. exists e; auto. } destruct H2; red in H2; simpl in H2; discriminate. + destruct 1. assert (Equivb cmp m1 m'1). { split. - intros k; generalize (H (xO k)); unfold In, MapsTo; simpl; auto. - intros k e e'; generalize (H0 (xO k) e e'); unfold In, MapsTo; simpl; auto. } assert (Equivb cmp m2 m'2). { split. - intros k; generalize (H (xI k)); unfold In, MapsTo; simpl; auto. - intros k e e'; generalize (H0 (xI k) e e'); unfold In, MapsTo; simpl; auto. } simpl. destruct o; destruct o0; simpl. * repeat (apply andb_true_intro; split); auto. apply (H0 xH); red; auto. * generalize (H xH); unfold In, MapsTo; simpl; intuition. destruct H4; try discriminate; eauto. * generalize (H xH); unfold In, MapsTo; simpl; intuition. destruct H5; try discriminate; eauto. * apply andb_true_intro; split; auto. Qed.
imports: Bool OrderedType ZArith OrderedType OrderedTypeEx FMapInterface