proposition: Lemma set_mem_correct2 : forall (a:A) (x:set), set_In a x -> set_mem a x = true.
proof: Proof. simple induction x; simpl. - intro Ha; elim Ha. - intros a0 l; elim (Aeq_dec a a0); auto with datatypes. intros H1 H2 [H3| H4]. + absurd (a0 = a); auto with datatypes. + auto with datatypes. Qed.
imports: List