proposition: Lemma mem_1 : forall m (Hm:Sort m) x, In x m -> mem x m = true.
proof: Proof. intros m Hm x; generalize Hm; clear Hm. induction m as [ |[k' _x] l IHb]; intros sorted belong1. - inversion belong1. inversion H. - simpl. case_eq (compare x k'); trivial. + intros _x0 e0. absurd (In x ((k', _x) :: l));try assumption. apply Sort_Inf_NotIn with _x;auto with smtcoq_array. + intros _x0 e0. apply IHb. elim (sort_inv sorted);auto with smtcoq_array. elim (In_inv belong1);auto with smtcoq_array. intro abs. absurd (eq x k'); auto with smtcoq_array. symmetry in abs. apply lt_not_eq in abs; auto with smtcoq_array. Qed.
imports: Bool OrderedType SMT_classes ProofIrrelevance