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 as (E,_); simpl. red in E. apply is_empty_spec; intros k. destruct (find k m') eqn:F; trivial. assert (H : In k m') by now exists a. rewrite <- E in H. destruct H as (x,H). red in H. now rewrite gleaf in H. - destruct m'. + destruct 1 as (E,_); simpl. red in E. destruct o. * assert (H : In xH (@Leaf A)). { rewrite <- E. now exists a. } destruct H as (e,H). now red in H. * apply andb_true_intro; split; apply is_empty_spec; intros k. destruct (find k m1) eqn:F; trivial. assert (H : In (xO k) (@Leaf A)). { rewrite <- E. exists a; auto. } destruct H as (x,H). red in H. now rewrite gleaf in H. destruct (find k m2) eqn:F; trivial. assert (H : In (xI k) (@Leaf A)). { rewrite <- E. exists a; auto. } destruct H as (x,H). red in H. now rewrite gleaf in H. + 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: Coq(Bool PeanoNat BinPos Orders OrdersEx OrdersLists) MMaps(Utils Comparisons Interface)