proposition: Lemma mem_2 : forall m (Hm:Sort m) x, mem x m = true -> In x m.
proof: Proof. intros m Hm; induction m as [|[a m]]; intros x H; simpl in *. - discriminate. - destruct X.compare; [discriminate| |]. + exists m; apply InA_cons_hd; split; auto. + inversion_clear Hm; destruct IHm with x as [e He]; auto. exists e; apply InA_cons_tl; auto. Qed.
imports: FMapInterface