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. functional induction (mem x m); intros sorted hyp;try ((inversion hyp);fail). exists _x; auto. induction IHb; auto. exists x0; auto. inversion_clear sorted; auto. Qed.
imports: SetoidList Bool OrderedType OrdersLists RelationPairs Orders RelationClasses