proposition: Lemma equal_1 : forall m (Hm:Sort m) m' (Hm': Sort m') cmp, Equivb cmp m m' -> equal cmp m m' = true.
proof: Proof. intros m Hm m' Hm' cmp; generalize Hm Hm'; clear Hm Hm'. revert m'; induction m as [ |[x e] l IHl]; intros [ |[x' e'] l']; simpl; auto with smtcoq_array; unfold Equivb; intuition; subst. - destruct (H0 x') as [_ H3]. assert (H2: In x' nil). { apply H3. exists e'. now constructor. } elim H2. intros x Hx. inversion Hx. - destruct (H0 x) as [H3 _]. assert (H2: In x nil). { apply H3. exists e. now constructor. } elim H2. intros x0 Hx0. inversion Hx0. - case_eq (compare x x'); simpl; subst;auto with smtcoq_array; unfold Equivb; intuition; subst. + destruct (H0 x). assert (In x ((x',e')::l')). apply H2; auto with smtcoq_array. exists e; auto with smtcoq_array. destruct (In_inv H4). clear H. apply lt_not_eq in l0; now contradict l0. inversion_clear Hm'. assert (Inf (x,e) l'). apply Inf_lt with (x',e'); auto with smtcoq_array. elim (Sort_Inf_NotIn H6 H8 H5). + match goal with H: compare _ _ = _ |- _ => clear H end. assert (cmp_e_e':cmp e e' = true). apply H1 with x'; auto with smtcoq_array. rewrite cmp_e_e'; simpl. apply IHl; auto with smtcoq_array. inversion_clear Hm; auto with smtcoq_array. inversion_clear Hm'; auto with smtcoq_array. unfold Equivb; intuition. destruct (H0 k). assert (In k ((x',e) ::l)). destruct H as (e'', hyp); exists e''; auto with smtcoq_array. destruct (In_inv (H2 H4)); auto with smtcoq_array. inversion_clear Hm. elim (Sort_Inf_NotIn H6 H7). destruct H as (e'', hyp); exists e''; auto with smtcoq_array. apply MapsTo_eq with k; auto with smtcoq_array. destruct (H0 k). assert (In k ((x',e') ::l')). destruct H as (e'', hyp); exists e''; auto with smtcoq_array. destruct (In_inv (H3 H4)); auto with smtcoq_array. subst. inversion_clear Hm'. now elim (Sort_Inf_NotIn H5 H6). apply H1 with k; destruct (eq_dec x' k); auto with smtcoq_array. + destruct (H0 x'). assert (In x' ((x,e)::l)). apply H3; auto with smtcoq_array. exists e'; auto with smtcoq_array. destruct (In_inv H4). clear H; subst; apply lt_not_eq in l0; now contradict l0. inversion_clear Hm. assert (Inf (x',e') l). apply Inf_lt with (x,e); auto with smtcoq_array. elim (Sort_Inf_NotIn H6 H8 H5). Qed.
imports: Bool OrderedType SMT_classes ProofIrrelevance