proposition: Lemma mem_2 : forall m (Hm:Sort m) x, mem x m = true -> In x m.
proof: Proof. intros m Hm x; generalize Hm; clear Hm; unfold In,MapsTo. induction m as [ |[k' _x] l IHb]; intros sorted hyp;try ((inversion hyp);fail). revert hyp. simpl. case_eq (compare x k'); intros _x0 e0 hyp;try ((inversion hyp);fail). - exists _x; auto with smtcoq_array. - induction IHb; auto with smtcoq_array. + exists x0; auto with smtcoq_array. + inversion_clear sorted; auto with smtcoq_array. Qed.
imports: Bool OrderedType SMT_classes ProofIrrelevance