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