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. functional induction (mem x m);intros sorted belong1;trivial. inversion belong1. inversion H. absurd (In x ((k', _x) :: l));try assumption. apply Sort_Inf_NotIn with _x;auto. apply IHb. elim (sort_inv sorted);auto. elim (In_inv belong1);auto. intro abs. absurd (eq x k'); auto. symmetry in abs. apply lt_not_eq in abs; auto. Qed.
imports: SetoidList Bool OrderedType OrdersLists RelationPairs Orders RelationClasses