proposition: Lemma mem_3 : forall m (Hm:Sort m) x, mem x m = false -> ~ In x m.
proof: Proof. intros. rewrite <- not_true_iff_false in H. unfold not in *. intros; apply H. now apply mem_1. Qed.
imports: Bool OrderedType SMT_classes ProofIrrelevance