proposition: Lemma equal_2 : forall m (Hm:Sort m) m' (Hm:Sort m') cmp, equal cmp m m' = true -> Equivb cmp m m'.
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; subst;auto with smtcoq_array; unfold Equivb; intuition; try discriminate; subst; try match goal with H: compare _ _ = _ |- _ => clear H end. - inversion H0. - revert H; case_eq (compare x x'); intros _x _ H; try inversion H. inversion_clear Hm;inversion_clear Hm'. destruct (andb_prop _ _ H); clear H. destruct (IHl _ H1 H4 H7). destruct (In_inv H0). exists e'; constructor; split; trivial; apply eq_trans with x; auto with smtcoq_array. destruct (H k). destruct (H10 H9) as (e'',hyp). exists e''; auto with smtcoq_array. - revert H; case_eq (compare x x'); intros _x _ H; try inversion H. inversion_clear Hm;inversion_clear Hm'. destruct (andb_prop _ _ H); clear H. destruct (IHl _ H1 H4 H7). destruct (In_inv H0). exists e; constructor; split; trivial; apply eq_trans with x'; auto with smtcoq_array. destruct (H k). destruct (H11 H9) as (e'',hyp). exists e''; auto with smtcoq_array. - revert H; case_eq (compare x x'); intros _x _ H; [inversion H| |inversion H]. inversion_clear Hm;inversion_clear Hm'. destruct (andb_prop _ _ H); clear H. destruct (IHl _ H2 H4 H7). inversion_clear H0. + destruct H9; simpl in *; subst. inversion_clear H1. * destruct H0; simpl in *; subst; auto with smtcoq_array. * elim (Sort_Inf_NotIn H4 H5). exists e'0; apply MapsTo_eq with x'; auto with smtcoq_array. + inversion_clear H1. * destruct H0; simpl in *; subst; auto with smtcoq_array. elim (Sort_Inf_NotIn H2 H3). exists e0; apply MapsTo_eq with x'; auto with smtcoq_array. * apply H8 with k; auto with smtcoq_array. Qed.
imports: Bool OrderedType SMT_classes ProofIrrelevance