proposition: Lemma set_mem_complete1 : forall (a:A) (x:set), set_mem a x = false -> ~ set_In a x.
proof: Proof. simple induction x; simpl. - tauto. - intros a0 l; elim (Aeq_dec a a0). + intros _ _ [=]. + unfold not; intros H H0 H1 [|]; auto with datatypes. Qed.
imports: List